Metamath Proof Explorer

Theorem elxp2

Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004) (Proof shortened by JJ, 13-Aug-2021)

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

Proof

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