Definition df-xp 4685

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

This definition is referenced by:  xpeq1  4693  xpeq2  4694  elxpi  4695  elxp  4696  nfxp  4706  fconstmpt  4726  brab2a  4732  xpundi  4735  xpundir  4736  opabssxp  4753  csbxpg  4760  xpss12  4786  relopabiv  4805  inxp  4816  dmxpm  4903  dmxpid  4904  resopab  5008  cnvxp  5106  xpcom  5234  dfxp3  6287  dmaddpq  7499  dmmulpq  7500  enq0enq  7551  npsspw  7591  shftfvalg  11173  shftfval  11176  eqgfval  13602  reldvdsrsrg  13898  dvdsrvald  13899  dvdsrex  13904  lgsquadlem3  15600