Metamath Proof Explorer

Theorem elxpi

Description: Membership in a Cartesian product. Uses fewer axioms than elxp . (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion elxpi 
|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( z = w -> ( z = <. x , y >. <-> w = <. x , y >. ) )
2 1 anbi1d 
 |-  ( z = w -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
3 2 2exbidv 
 |-  ( z = w -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
4 eqeq1 
 |-  ( w = A -> ( w = <. x , y >. <-> A = <. x , y >. ) )
5 4 anbi1d 
 |-  ( w = A -> ( ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
6 5 2exbidv 
 |-  ( w = A -> ( E. x E. y ( w = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
7 df-xp 
 |-  ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
8 df-opab 
 |-  { <. x , y >. | ( x e. B /\ y e. C ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
9 7 8 eqtri 
 |-  ( B X. C ) = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
10 3 6 9 elab2gw 
 |-  ( A e. ( B X. C ) -> ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
11 10 ibi 
 |-  ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )