Theorem elaltxp

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

	Ref	Expression
Assertion	elaltxp	$$⊢X\in \left(A\mathrm{\times \times }B\right)\leftrightarrow \exists x\in A\exists y\in BX=⟪x,y⟫$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢X\in \left(A\mathrm{\times \times }B\right)\to X\in \mathrm{V}$$
2		altopex	$$⊢⟪x,y⟫\in \mathrm{V}$$
3		eleq1	$$⊢X=⟪x,y⟫\to \left(X\in \mathrm{V}\leftrightarrow ⟪x,y⟫\in \mathrm{V}\right)$$
4	2 3	mpbiri	$$⊢X=⟪x,y⟫\to X\in \mathrm{V}$$
5	4	a1i	$$⊢\left(x\in A\wedge y\in B\right)\to \left(X=⟪x,y⟫\to X\in \mathrm{V}\right)$$
6	5	rexlimivv	$$⊢\exists x\in A\exists y\in BX=⟪x,y⟫\to X\in \mathrm{V}$$
7		eqeq1	$$⊢z=X\to \left(z=⟪x,y⟫\leftrightarrow X=⟪x,y⟫\right)$$
8	7	2rexbidv	$$⊢z=X\to \left(\exists x\in A\exists y\in Bz=⟪x,y⟫\leftrightarrow \exists x\in A\exists y\in BX=⟪x,y⟫\right)$$
9		df-altxp	$$⊢\left(A\mathrm{\times \times }B\right)=\left\{z|\exists x\in A\exists y\in Bz=⟪x,y⟫\right\}$$
10	8 9	elab2g	$$⊢X\in \mathrm{V}\to \left(X\in \left(A\mathrm{\times \times }B\right)\leftrightarrow \exists x\in A\exists y\in BX=⟪x,y⟫\right)$$
11	1 6 10	pm5.21nii	$$⊢X\in \left(A\mathrm{\times \times }B\right)\leftrightarrow \exists x\in A\exists y\in BX=⟪x,y⟫$$