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