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 ) ) )