Definition df-xp 4731

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 4723	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1396	. . . . 5 class 𝑥
6	5, 1	wcel 2202	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1396	. . . . 5 class 𝑦
9	8, 2	wcel 2202	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4149	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1397	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4739  xpeq2  4740  elxpi  4741  elxp  4742  nfxp  4752  fconstmpt  4773  brab2a  4779  xpundi  4782  xpundir  4783  opabssxp  4800  csbxpg  4807  xpss12  4833  relopabiv  4853  inxp  4864  dmxpm  4952  dmxpid  4953  resopab  5057  cnvxp  5155  xpcom  5283  dfxp3  6359  dmaddpq  7599  dmmulpq  7600  enq0enq  7651  npsspw  7691  shftfvalg  11396  shftfval  11399  eqgfval  13827  dvdsrvald  14126  dvdsrex  14131  lgsquadlem3  15827