Metamath Proof Explorer

Theorem dfoprab3s

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

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

Proof

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