Metamath Proof Explorer

Theorem dfopab2

Description: A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfopab2 
|- { <. x , y >. | ph } = { z e. ( _V X. _V ) | [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph }

Proof

Step Hyp Ref Expression
1 nfsbc1v 
 |-  F/ x [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph
2 1 19.41 
 |-  ( E. x ( E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) <-> ( E. x E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
3 sbcopeq1a 
 |-  ( z = <. x , y >. -> ( [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph <-> ph ) )
4 3 pm5.32i 
 |-  ( ( z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) <-> ( z = <. x , y >. /\ ph ) )
5 4 exbii 
 |-  ( E. y ( z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) <-> E. y ( z = <. x , y >. /\ ph ) )
6 nfcv 
 |-  F/_ y ( 1st ` z )
7 nfsbc1v 
 |-  F/ y [. ( 2nd ` z ) / y ]. ph
8 6 7 nfsbcw 
 |-  F/ y [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph
9 8 19.41 
 |-  ( E. y ( z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) <-> ( E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
10 5 9 bitr3i 
 |-  ( E. y ( z = <. x , y >. /\ ph ) <-> ( E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
11 10 exbii 
 |-  ( E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x ( E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
12 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. x E. y z = <. x , y >. )
13 12 anbi1i 
 |-  ( ( z e. ( _V X. _V ) /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) <-> ( E. x E. y z = <. x , y >. /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
14 2 11 13 3bitr4i 
 |-  ( E. x E. y ( z = <. x , y >. /\ ph ) <-> ( z e. ( _V X. _V ) /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) )
15 14 abbii 
 |-  { z | E. x E. y ( z = <. x , y >. /\ ph ) } = { z | ( z e. ( _V X. _V ) /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) }
16 df-opab 
 |-  { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
17 df-rab 
 |-  { z e. ( _V X. _V ) | [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph } = { z | ( z e. ( _V X. _V ) /\ [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph ) }
18 15 16 17 3eqtr4i 
 |-  { <. x , y >. | ph } = { z e. ( _V X. _V ) | [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph }