Definition df-xp 5595

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 28800). Another example is that the set of rational numbers is defined in df-q 12689 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 5587	. 2 class (𝐴 × 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6	5, 1	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7		vy	. . . . . 6 setvar 𝑦
8	7	cv 1538	. . . . 5 class 𝑦
9	8, 2	wcel 2106	. . . 4 wff 𝑦 ∈ 𝐵
10	6, 9	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
11	10, 4, 7	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
12	3, 11	wceq 1539	1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}

This definition is referenced by:  xpeq1  5603  xpss12  5604  xpeq2  5610  elxpi  5611  elxp  5612  nfxp  5622  fconstmpt  5649  xpundi  5655  xpundir  5656  elopaelxp  5676  opabssxp  5679  csbxp  5686  ssrel  5693  ssrelOLD  5694  relopabiv  5730  relopabi  5732  inxp  5741  dmxp  5838  resopab  5942  cnvxp  6060  xpco  6192  1st2val  7859  2nd2val  7860  dfxp3  7901  marypha2lem2  9195  wemapwe  9455  cardf2  9701  dfac3  9877  axdc2lem  10204  fpwwe2lem1  10387  canthwe  10407  xpcogend  14685  shftfval  14781  ipoval  18248  ipolerval  18250  eqgfval  18804  frgpuplem  19378  pjfval2  20916  ltbwe  21245  opsrtoslem1  21262  2ndcctbss  22606  ulmval  25539  lgsquadlem3  26530  iscgrg  26873  ishpg  27120  nvss  28955  ajfval  29171  fpwrelmap  31068  afsval  32651  cvmlift2lem12  33276  bj-opabssvv  35321  bj-xpcossxp  35360  dicval  39190  dnwech  40873  fgraphopab  41035  areaquad  41047  csbxpgVD  42514  relopabVD  42521  dfnelbr2  44765  xpsnopab  45319