Definition df-altxp

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

	Ref	Expression
Assertion	df-altxp	|- ( A XX. B ) = { z | E. x e. A E. y e. B z = << x , y >> }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	caltxp	|- ( A XX. B )
3		vz	|- z
4		vx	|- x
5		vy	|- y
6	3	cv	|- z
7	4	cv	|- x
8	5	cv	|- y
9	7 8	caltop	|- << x , y >>
10	6 9	wceq	|- z = << x , y >>
11	10 5 1	wrex	|- E. y e. B z = << x , y >>
12	11 4 0	wrex	|- E. x e. A E. y e. B z = << x , y >>
13	12 3	cab	|- { z | E. x e. A E. y e. B z = << x , y >> }
14	2 13	wceq	|- ( A XX. B ) = { z | E. x e. A E. y e. B z = << x , y >> }