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

Metamath Proof Explorer

Theorem elxp3

Description: Membership in a Cartesian product. (Contributed by NM, 5-Mar-1995)

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

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
2 eqcom 
 |-  ( <. x , y >. = A <-> A = <. x , y >. )
3 opelxp 
 |-  ( <. x , y >. e. ( B X. C ) <-> ( x e. B /\ y e. C ) )
4 2 3 anbi12i 
 |-  ( ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
5 4 2exbii 
 |-  ( E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
6 1 5 bitr4i 
 |-  ( A e. ( B X. C ) <-> E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) )