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 }