Metamath Proof Explorer

Theorem rabxp

Description: Class abstraction restricted to a Cartesian product as an ordered-pair class abstraction. (Contributed by NM, 20-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 rabxp.1 
 |-  ( x = <. y , z >. -> ( ph <-> ps ) )
2 elxp 
 |-  ( x e. ( A X. B ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) )
3 2 anbi1i 
 |-  ( ( x e. ( A X. B ) /\ ph ) <-> ( E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) )
4 19.41vv 
 |-  ( E. y E. z ( ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) <-> ( E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) )
5 anass 
 |-  ( ( ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) <-> ( x = <. y , z >. /\ ( ( y e. A /\ z e. B ) /\ ph ) ) )
6 1 anbi2d 
 |-  ( x = <. y , z >. -> ( ( ( y e. A /\ z e. B ) /\ ph ) <-> ( ( y e. A /\ z e. B ) /\ ps ) ) )
7 df-3an 
 |-  ( ( y e. A /\ z e. B /\ ps ) <-> ( ( y e. A /\ z e. B ) /\ ps ) )
8 6 7 bitr4di 
 |-  ( x = <. y , z >. -> ( ( ( y e. A /\ z e. B ) /\ ph ) <-> ( y e. A /\ z e. B /\ ps ) ) )
9 8 pm5.32i 
 |-  ( ( x = <. y , z >. /\ ( ( y e. A /\ z e. B ) /\ ph ) ) <-> ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) )
10 5 9 bitri 
 |-  ( ( ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) <-> ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) )
11 10 2exbii 
 |-  ( E. y E. z ( ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) /\ ph ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) )
12 3 4 11 3bitr2i 
 |-  ( ( x e. ( A X. B ) /\ ph ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) )
13 12 abbii 
 |-  { x | ( x e. ( A X. B ) /\ ph ) } = { x | E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) }
14 df-rab 
 |-  { x e. ( A X. B ) | ph } = { x | ( x e. ( A X. B ) /\ ph ) }
15 df-opab 
 |-  { <. y , z >. | ( y e. A /\ z e. B /\ ps ) } = { x | E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B /\ ps ) ) }
16 13 14 15 3eqtr4i 
 |-  { x e. ( A X. B ) | ph } = { <. y , z >. | ( y e. A /\ z e. B /\ ps ) }