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

Metamath Proof Explorer

Theorem dfoprab3

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis dfoprab3.1 
|- ( w = <. x , y >. -> ( ph <-> ps ) )
Assertion dfoprab3 
|- { <. w , z >. | ( w e. ( _V X. _V ) /\ ph ) } = { <. <. x , y >. , z >. | ps }

Proof

Step Hyp Ref Expression
1 dfoprab3.1 
 |-  ( w = <. x , y >. -> ( ph <-> ps ) )
2 dfoprab3s 
 |-  { <. <. x , y >. , z >. | ps } = { <. w , z >. | ( w e. ( _V X. _V ) /\ [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ps ) }
3 fvex 
 |-  ( 1st ` w ) e. _V
4 fvex 
 |-  ( 2nd ` w ) e. _V
5 eqcom 
 |-  ( x = ( 1st ` w ) <-> ( 1st ` w ) = x )
6 eqcom 
 |-  ( y = ( 2nd ` w ) <-> ( 2nd ` w ) = y )
7 5 6 anbi12i 
 |-  ( ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) <-> ( ( 1st ` w ) = x /\ ( 2nd ` w ) = y ) )
8 eqopi 
 |-  ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) = x /\ ( 2nd ` w ) = y ) ) -> w = <. x , y >. )
9 7 8 sylan2b 
 |-  ( ( w e. ( _V X. _V ) /\ ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> w = <. x , y >. )
10 9 1 syl 
 |-  ( ( w e. ( _V X. _V ) /\ ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> ( ph <-> ps ) )
11 10 bicomd 
 |-  ( ( w e. ( _V X. _V ) /\ ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> ( ps <-> ph ) )
12 11 ex 
 |-  ( w e. ( _V X. _V ) -> ( ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( ps <-> ph ) ) )
13 3 4 12 sbc2iedv 
 |-  ( w e. ( _V X. _V ) -> ( [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ps <-> ph ) )
14 13 pm5.32i 
 |-  ( ( w e. ( _V X. _V ) /\ [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ps ) <-> ( w e. ( _V X. _V ) /\ ph ) )
15 14 opabbii 
 |-  { <. w , z >. | ( w e. ( _V X. _V ) /\ [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ps ) } = { <. w , z >. | ( w e. ( _V X. _V ) /\ ph ) }
16 2 15 eqtr2i 
 |-  { <. w , z >. | ( w e. ( _V X. _V ) /\ ph ) } = { <. <. x , y >. , z >. | ps }