Definition df-xp 5033

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⟩}) (ex-xp 26478). Another example is that the set of rational numbers are defined in df-q 11623 using the Cartesian product (ℤ × ℕ); 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 5025	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1473	. . . . 5 class 𝑥
6	5, 1	wcel 1976	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1473	. . . . 5 class 𝑦
9	8, 2	wcel 1976	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 382	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 4636	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1474	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5041  xpeq2  5042  elxpi  5043  elxp  5044  nfxp  5055  fconstmpt  5074  brab2a  5080  xpundi  5083  xpundir  5084  opabssxp  5105  csbxp  5112  xpss12  5136  inxp  5163  dmxp  5251  resopab  5352  cnvxp  5455  xpco  5577  1st2val  7062  2nd2val  7063  dfxp3  7096  marypha2lem2  8202  wemapwe  8454  cardf2  8629  dfac3  8804  axdc2lem  9130  fpwwe2lem1  9309  canthwe  9329  xpcogend  13509  shftfval  13606  ipoval  16925  ipolerval  16927  eqgfval  17413  frgpuplem  17956  ltbwe  19241  opsrtoslem1  19253  pjfval2  19819  2ndcctbss  21015  ulmval  23882  lgsquadlem3  24851  iscgrg  25152  ishpg  25396  iseupa  26285  nvss  26625  ajfval  26841  fpwrelmap  28689  afsval  29795  cvmlift2lem12  30343  dicval  35266  dnwech  36419  fgraphopab  36590  areaquad  36604  csbxpgOLD  37858  csbxpgVD  37935  relopabVD  37942  xpsnopab  41536