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 ×k B) = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ 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 ×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 ∈ A
13	9, 2	wcel 1710	. . . . . . 7 wff z ∈ B
14	12, 13	wa 358	. . . . . 6 wff (y ∈ A ∧ z ∈ B)
15	11, 14	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))
16	15, 8	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))
17	16, 6	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))
18	17, 4	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))}
19	3, 18	wceq 1642	1 wff (A ×k B) = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ (y ∈ A ∧ z ∈ B))}

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