Definition df-altxp 32066

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

Assertion

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

Distinct variable groups:   x, A, y, z   x, B, y, z

Detailed syntax breakdown of Definition df-altxp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	caltxp 32064	. 2 class ( A XX. B )
4		vz	. . . . . . 7 setvar z
5	4	cv 1482	. . . . . 6 class z
6		vx	. . . . . . . 8 setvar x
7	6	cv 1482	. . . . . . 7 class x
8		vy	. . . . . . . 8 setvar y
9	8	cv 1482	. . . . . . 7 class y
10	7, 9	caltop 32063	. . . . . 6 class << x , y >>
11	5, 10	wceq 1483	. . . . 5 wff z = << x , y >>
12	11, 8, 2	wrex 2913	. . . 4 wff E. y e. B z = << x , y >>
13	12, 6, 1	wrex 2913	. . 3 wff E. x e. A E. y e. B z = << x , y >>
14	13, 4	cab 2608	. 2 class { z | E. x e. A E. y e. B z = << x , y >> }
15	3, 14	wceq 1483	1 wff ( A XX. B ) = { z | E. x e. A E. y e. B z = << x , y >> }

This definition is referenced by:  altxpeq1  32080  altxpeq2  32081  elaltxp  32082