Definition df-altxp

Description: Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012)

	Ref	Expression
Assertion	df-altxp	$$⊢\left(A\mathrm{\times \times }B\right)=\left\{z|\exists x\in A\exists y\in Bz=⟪x,y⟫\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	caltxp	$$class\left(A\mathrm{\times \times }B\right)$$
3		vz	$$setvarz$$
4		vx	$$setvarx$$
5		vy	$$setvary$$
6	3	cv	$$setvarz$$
7	4	cv	$$setvarx$$
8	5	cv	$$setvary$$
9	7 8	caltop	$$class⟪x,y⟫$$
10	6 9	wceq	$$wffz=⟪x,y⟫$$
11	10 5 1	wrex	$$wff\exists y\in Bz=⟪x,y⟫$$
12	11 4 0	wrex	$$wff\exists x\in A\exists y\in Bz=⟪x,y⟫$$
13	12 3	cab	$$class\left\{z|\exists x\in A\exists y\in Bz=⟪x,y⟫\right\}$$
14	2 13	wceq	$$wff\left(A\mathrm{\times \times }B\right)=\left\{z|\exists x\in A\exists y\in Bz=⟪x,y⟫\right\}$$