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

Metamath Proof Explorer

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 ) }