Theorem dfoprab4

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dfoprab4.1	|- ( w = <. x , y >. -> ( ph <-> ps ) )
2		xpss	|- ( A X. B ) C_ ( _V X. _V )
3	2	sseli	|- ( w e. ( A X. B ) -> w e. ( _V X. _V ) )
4	3	adantr	|- ( ( w e. ( A X. B ) /\ ph ) -> w e. ( _V X. _V ) )
5	4	pm4.71ri	|- ( ( w e. ( A X. B ) /\ ph ) <-> ( w e. ( _V X. _V ) /\ ( w e. ( A X. B ) /\ ph ) ) )
6	5	opabbii	|- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. w , z >. | ( w e. ( _V X. _V ) /\ ( w e. ( A X. B ) /\ ph ) ) }
7		eleq1	|- ( w = <. x , y >. -> ( w e. ( A X. B ) <-> <. x , y >. e. ( A X. B ) ) )
8		opelxp	|- ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
9	7 8	bitrdi	|- ( w = <. x , y >. -> ( w e. ( A X. B ) <-> ( x e. A /\ y e. B ) ) )
10	9 1	anbi12d	|- ( w = <. x , y >. -> ( ( w e. ( A X. B ) /\ ph ) <-> ( ( x e. A /\ y e. B ) /\ ps ) ) )
11	10	dfoprab3	|- { <. w , z >. | ( w e. ( _V X. _V ) /\ ( w e. ( A X. B ) /\ ph ) ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }
12	6 11	eqtri	|- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }