Theorem elxpi

Description: Membership in a Cartesian product. Uses fewer axioms than elxp . (Contributed by NM, 4-Jul-1994)

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

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( z = A -> ( z = <. x , y >. <-> A = <. x , y >. ) )
2	1	anbi1d	|- ( z = A -> ( ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
3	2	2exbidv	|- ( z = A -> ( E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
4		df-xp	|- ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
5		df-opab	|- { <. x , y >. | ( x e. B /\ y e. C ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
6	4 5	eqtri	|- ( B X. C ) = { z | E. x E. y ( z = <. x , y >. /\ ( x e. B /\ y e. C ) ) }
7	3 6	elab2g	|- ( A e. ( B X. C ) -> ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) ) )
8	7	ibi	|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )