Definition df-xp 2424

Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64.

Assertion

Ref	Expression
df-xp	⊢ (A × B) = {⟨x, y⟩∣(x ∈ A ∧ y ∈ B)}

Distinct variable group(s):   x,y,A   x,B,y

Detailed syntax breakdown of Definition df-xp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cxp 2408	. 2 class (A × B)
4		vx	. . . . . 6 set x
5	4	cv 1089	. . . . 5 class x
6	5, 1	wcel 1092	. . . 4 wff x ∈ A
7		vy	. . . . . 6 set y
8	7	cv 1089	. . . . 5 class y
9	8, 2	wcel 1092	. . . 4 wff y ∈ B
10	6, 9	wa 196	. . 3 wff (x ∈ A ∧ y ∈ B)
11	10, 4, 7	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ A ∧ y ∈ B)}
12	3, 11	wceq 1091	1 wff (A × B) = {⟨x, y⟩∣(x ∈ A ∧ y ∈ B)}

This definition is referenced by:  xpeq1 2440  xpeq2 2441  elxp 2442  fconstopab 2448  xpundi 2461  xpundir 2462  opabssxp 2468  relopab 2494  dmxp 2552  resopab 2598  fnoprab2 3039  1st2val 3097  aceq3 3556  genpdm 3899  infmap2lem2 4952

metamath.org