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

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 = A -> ( z = <. x , y >. <-> A = <. x , y >. ) )
2 1 anbi1d 
 |-  ( z = A -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
3 2 2exbidv 
 |-  ( z = A -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
4 df-xp 
 |-  ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
5 df-opab 
 |-  { <. x , y >. | ( x e. B /\ y e. C ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
6 4 5 eqtri 
 |-  ( B X. C ) = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
7 3 6 elab2g 
 |-  ( A e. ( B X. C ) -> ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
8 7 ibi 
 |-  ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )