Theorem elxp

Description: Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994)

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

Proof

Step	Hyp	Ref	Expression
1		df-xp	|- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
2	1	eleq2i	|- ( A e. ( B X. C ) <-> A e. { <. x , y >. | ( x e. B /\ y e. C ) } )
3		elopab	|- ( A e. { <. x , y >. | ( x e. B /\ y e. C ) } <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
4	2 3	bitri	|- ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )