Definition df-xp 4726

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

This definition is referenced by:  xpeq1  4734  xpeq2  4735  elxpi  4736  elxp  4737  nfxp  4747  fconstmpt  4768  brab2a  4774  xpundi  4777  xpundir  4778  opabssxp  4795  csbxpg  4802  xpss12  4828  relopabiv  4848  inxp  4859  dmxpm  4947  dmxpid  4948  resopab  5052  cnvxp  5150  xpcom  5278  dfxp3  6351  dmaddpq  7582  dmmulpq  7583  enq0enq  7634  npsspw  7674  shftfvalg  11350  shftfval  11353  eqgfval  13780  dvdsrvald  14078  dvdsrex  14083  lgsquadlem3  15779