set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ;
set C = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ;
for a being object holds
( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } )
proof
let a be
object ;
( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } )
hereby ( a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } implies a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } )
assume
a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
;
a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } then consider u being
Element of
F1(),
v being
Element of
F2()
such that A2:
a = F3(
u,
v)
and A3:
P1[
u,
v]
;
a = F4(
u,
v)
by A1, A2, A3;
hence
a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] }
by A3;
verum
end;
assume
a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] }
;
a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
then consider u being
Element of
F1(),
v being
Element of
F2()
such that A4:
a = F4(
u,
v)
and A5:
P1[
u,
v]
;
a = F3(
u,
v)
by A1, A4, A5;
hence
a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
by A5;
verum
end;
hence
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
by TARSKI:2; verum