Definition df-xp 4727

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 4719	. 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 4145	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1395	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  4735  xpeq2  4736  elxpi  4737  elxp  4738  nfxp  4748  fconstmpt  4769  brab2a  4775  xpundi  4778  xpundir  4779  opabssxp  4796  csbxpg  4803  xpss12  4829  relopabiv  4849  inxp  4860  dmxpm  4948  dmxpid  4949  resopab  5053  cnvxp  5151  xpcom  5279  dfxp3  6352  dmaddpq  7587  dmmulpq  7588  enq0enq  7639  npsspw  7679  shftfvalg  11366  shftfval  11369  eqgfval  13796  dvdsrvald  14094  dvdsrex  14099  lgsquadlem3  15795