Definition df-xp 5622

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 30411). Another example is that the set of rational numbers is defined in df-q 12844 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 5614	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6	5, 1	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1540	. . . . 5 class 𝑦
9	8, 2	wcel 2111	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5153	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1541	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5630  xpss12  5631  xpeq2  5637  elxpi  5638  elxp  5639  nfxp  5649  fconstmpt  5678  xpundi  5685  xpundir  5686  elopaelxp  5706  opabssxp  5708  csbxp  5716  ssrel  5723  relopabiv  5760  relopabi  5762  inxpOLD  5772  resopab  5983  cnvxp  6104  xpco  6236  1st2val  7949  2nd2val  7950  dfxp3  7993  marypha2lem2  9320  wemapwe  9587  cardf2  9833  dfac3  10009  axdc2lem  10336  fpwwe2lem1  10519  canthwe  10539  xpcogend  14878  shftfval  14974  ipoval  18433  ipolerval  18435  eqgfval  19086  frgpuplem  19682  pjfval2  21644  ltbwe  21977  opsrtoslem1  21988  2ndcctbss  23368  ulmval  26314  lgsquadlem3  27318  iscgrg  28488  ishpg  28735  nvss  30568  ajfval  30784  fpwrelmap  32711  afsval  34679  cvmlift2lem12  35346  bj-opabssvv  37183  bj-xpcossxp  37222  dicval  41214  dnwech  43080  fgraphopab  43235  areaquad  43248  csbxpgVD  44925  relopabVD  44932  dfnelbr2  47303  xpsnopab  48187