Definition df-xp 4617

Description: Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of [Quine] p. 64. For example, ({1, 5} × {2, 7}) = ({⟨1, 2⟩, ⟨1, 7⟩} ∪ {⟨5, 2⟩, ⟨5, 7⟩}). Another example is that the set of rational numbers is defined using the Cartesian product as (ℤ × ℕ); the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-xp	⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Detailed syntax breakdown of Definition df-xp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cxp 4609	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1347	. . . . 5 class 𝑥
6	5, 1	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1347	. . . . 5 class 𝑦
9	8, 2	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4049	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1348	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4625  xpeq2  4626  elxpi  4627  elxp  4628  nfxp  4638  fconstmpt  4658  brab2a  4664  xpundi  4667  xpundir  4668  opabssxp  4685  csbxpg  4692  xpss12  4718  inxp  4745  dmxpm  4831  dmxpid  4832  resopab  4935  cnvxp  5029  xpcom  5157  dfxp3  6173  dmaddpq  7341  dmmulpq  7342  enq0enq  7393  npsspw  7433  shftfvalg  10782  shftfval  10785