let st1 be set ; :: thesis: ( st1 in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₁[s1,t1] } implies P₂[st1] )
assume st1 in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₁[s1,t1] } ; :: thesis: P₂[st1]
then ex s1 being Element of F₁() ex t1 being Element of F₂() st
( st1 = F₃(s1,t1) & P₁[s1,t1] ) ;
hence P₂[st1] by A1; :: thesis: verum