Definition df-xpk 4186

Description: Define the Kuratowski cross product. This definition through df-idk 4196 set up the Kuratowski relationships. These are used mainly to prove the properties of df-op 4567, and are not used thereafter. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-xpk	|- (A X.k B) = {x | E.yE.z(x = <<y, z>> /\ (y e. A /\ z e. B))}

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

Detailed syntax breakdown of Definition df-xpk

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cxpk 4175	. 2 class (A X.k B)
4		vx	. . . . . . . 8 setvar x
5	4	cv 1641	. . . . . . 7 class x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1641	. . . . . . . 8 class y
8		vz	. . . . . . . . 9 setvar z
9	8	cv 1641	. . . . . . . 8 class z
10	7, 9	copk 4058	. . . . . . 7 class <<y, z>>
11	5, 10	wceq 1642	. . . . . 6 wff x = <<y, z>>
12	7, 1	wcel 1710	. . . . . . 7 wff y e. A
13	9, 2	wcel 1710	. . . . . . 7 wff z e. B
14	12, 13	wa 358	. . . . . 6 wff (y e. A /\ z e. B)
15	11, 14	wa 358	. . . . 5 wff (x = <<y, z>> /\ (y e. A /\ z e. B))
16	15, 8	wex 1541	. . . 4 wff E.z(x = <<y, z>> /\ (y e. A /\ z e. B))
17	16, 6	wex 1541	. . 3 wff E.yE.z(x = <<y, z>> /\ (y e. A /\ z e. B))
18	17, 4	cab 2339	. 2 class {x | E.yE.z(x = <<y, z>> /\ (y e. A /\ z e. B))}
19	3, 18	wceq 1642	1 wff (A X.k B) = {x | E.yE.z(x = <<y, z>> /\ (y e. A /\ z e. B))}

This definition is referenced by:  elxpk  4197  xpkssvvk  4211  opkelxpkg  4248