Theorem elaltxp

Description: Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( X e. ( A XX. B ) -> X e. _V )
2		altopex	|- << x , y >> e. _V
3		eleq1	|- ( X = << x , y >> -> ( X e. _V <-> << x , y >> e. _V ) )
4	2 3	mpbiri	|- ( X = << x , y >> -> X e. _V )
5	4	a1i	|- ( ( x e. A /\ y e. B ) -> ( X = << x , y >> -> X e. _V ) )
6	5	rexlimivv	|- ( E. x e. A E. y e. B X = << x , y >> -> X e. _V )
7		eqeq1	|- ( z = X -> ( z = << x , y >> <-> X = << x , y >> ) )
8	7	2rexbidv	|- ( z = X -> ( E. x e. A E. y e. B z = << x , y >> <-> E. x e. A E. y e. B X = << x , y >> ) )
9		df-altxp	|- ( A XX. B ) = { z | E. x e. A E. y e. B z = << x , y >> }
10	8 9	elab2g	|- ( X e. _V -> ( X e. ( A XX. B ) <-> E. x e. A E. y e. B X = << x , y >> ) )
11	1 6 10	pm5.21nii	|- ( X e. ( A XX. B ) <-> E. x e. A E. y e. B X = << x , y >> )