This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfoprab4f

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses dfoprab4f.x 
|- F/ x ph
dfoprab4f.y 
|- F/ y ph
dfoprab4f.1 
|- ( w = <. x , y >. -> ( ph <-> ps ) )
Assertion dfoprab4f 
|- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }

Proof

Step Hyp Ref Expression
1 dfoprab4f.x 
 |-  F/ x ph
2 dfoprab4f.y 
 |-  F/ y ph
3 dfoprab4f.1 
 |-  ( w = <. x , y >. -> ( ph <-> ps ) )
4 nfv 
 |-  F/ x w = <. t , u >.
5 nfs1v 
 |-  F/ x [ t / x ] [ u / y ] ps
6 1 5 nfbi 
 |-  F/ x ( ph <-> [ t / x ] [ u / y ] ps )
7 4 6 nfim 
 |-  F/ x ( w = <. t , u >. -> ( ph <-> [ t / x ] [ u / y ] ps ) )
8 opeq1 
 |-  ( x = t -> <. x , u >. = <. t , u >. )
9 8 eqeq2d 
 |-  ( x = t -> ( w = <. x , u >. <-> w = <. t , u >. ) )
10 sbequ12 
 |-  ( x = t -> ( [ u / y ] ps <-> [ t / x ] [ u / y ] ps ) )
11 10 bibi2d 
 |-  ( x = t -> ( ( ph <-> [ u / y ] ps ) <-> ( ph <-> [ t / x ] [ u / y ] ps ) ) )
12 9 11 imbi12d 
 |-  ( x = t -> ( ( w = <. x , u >. -> ( ph <-> [ u / y ] ps ) ) <-> ( w = <. t , u >. -> ( ph <-> [ t / x ] [ u / y ] ps ) ) ) )
13 nfv 
 |-  F/ y w = <. x , u >.
14 nfs1v 
 |-  F/ y [ u / y ] ps
15 2 14 nfbi 
 |-  F/ y ( ph <-> [ u / y ] ps )
16 13 15 nfim 
 |-  F/ y ( w = <. x , u >. -> ( ph <-> [ u / y ] ps ) )
17 opeq2 
 |-  ( y = u -> <. x , y >. = <. x , u >. )
18 17 eqeq2d 
 |-  ( y = u -> ( w = <. x , y >. <-> w = <. x , u >. ) )
19 sbequ12 
 |-  ( y = u -> ( ps <-> [ u / y ] ps ) )
20 19 bibi2d 
 |-  ( y = u -> ( ( ph <-> ps ) <-> ( ph <-> [ u / y ] ps ) ) )
21 18 20 imbi12d 
 |-  ( y = u -> ( ( w = <. x , y >. -> ( ph <-> ps ) ) <-> ( w = <. x , u >. -> ( ph <-> [ u / y ] ps ) ) ) )
22 16 21 3 chvarfv 
 |-  ( w = <. x , u >. -> ( ph <-> [ u / y ] ps ) )
23 7 12 22 chvarfv 
 |-  ( w = <. t , u >. -> ( ph <-> [ t / x ] [ u / y ] ps ) )
24 23 dfoprab4 
 |-  { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. t , u >. , z >. | ( ( t e. A /\ u e. B ) /\ [ t / x ] [ u / y ] ps ) }
25 nfv 
 |-  F/ t ( ( x e. A /\ y e. B ) /\ ps )
26 nfv 
 |-  F/ u ( ( x e. A /\ y e. B ) /\ ps )
27 nfv 
 |-  F/ x ( t e. A /\ u e. B )
28 27 5 nfan 
 |-  F/ x ( ( t e. A /\ u e. B ) /\ [ t / x ] [ u / y ] ps )
29 nfv 
 |-  F/ y ( t e. A /\ u e. B )
30 14 nfsbv 
 |-  F/ y [ t / x ] [ u / y ] ps
31 29 30 nfan 
 |-  F/ y ( ( t e. A /\ u e. B ) /\ [ t / x ] [ u / y ] ps )
32 eleq1w 
 |-  ( x = t -> ( x e. A <-> t e. A ) )
33 eleq1w 
 |-  ( y = u -> ( y e. B <-> u e. B ) )
34 32 33 bi2anan9 
 |-  ( ( x = t /\ y = u ) -> ( ( x e. A /\ y e. B ) <-> ( t e. A /\ u e. B ) ) )
35 19 10 sylan9bbr 
 |-  ( ( x = t /\ y = u ) -> ( ps <-> [ t / x ] [ u / y ] ps ) )
36 34 35 anbi12d 
 |-  ( ( x = t /\ y = u ) -> ( ( ( x e. A /\ y e. B ) /\ ps ) <-> ( ( t e. A /\ u e. B ) /\ [ t / x ] [ u / y ] ps ) ) )
37 25 26 28 31 36 cbvoprab12 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } = { <. <. t , u >. , z >. | ( ( t e. A /\ u e. B ) /\ [ t / x ] [ u / y ] ps ) }
38 24 37 eqtr4i 
 |-  { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }