Definition df-xp 5629

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

This definition is referenced by:  xpeq1  5637  xpss12  5638  xpeq2  5644  elxpi  5645  elxp  5646  nfxp  5656  fconstmpt  5685  xpundi  5692  xpundir  5693  elopaelxp  5713  opabssxp  5715  csbxp  5723  ssrel  5730  relopabiv  5767  relopabi  5769  inxpOLD  5779  resopab  5989  cnvxp  6110  xpco  6241  1st2val  7959  2nd2val  7960  dfxp3  8003  marypha2lem2  9345  wemapwe  9612  cardf2  9858  dfac3  10034  axdc2lem  10361  fpwwe2lem1  10544  canthwe  10564  xpcogend  14899  shftfval  14995  ipoval  18454  ipolerval  18456  eqgfval  19073  frgpuplem  19669  pjfval2  21634  ltbwe  21967  opsrtoslem1  21978  2ndcctbss  23358  ulmval  26305  lgsquadlem3  27309  iscgrg  28475  ishpg  28722  nvss  30555  ajfval  30771  fpwrelmap  32689  afsval  34638  cvmlift2lem12  35286  bj-opabssvv  37123  bj-xpcossxp  37162  dicval  41155  dnwech  43021  fgraphopab  43176  areaquad  43189  csbxpgVD  44867  relopabVD  44874  dfnelbr2  47258  xpsnopab  48142