MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xp Structured version   Visualization version   GIF version

Definition df-xp 5684
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 30259). Another example is that the set of rational numbers is defined in df-q 12964 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cxp 5676 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1533 . . . . 5 class 𝑥
65, 1wcel 2099 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1533 . . . . 5 class 𝑦
98, 2wcel 2099 . . . 4 wff 𝑦𝐵
106, 9wa 395 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 5210 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1534 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5692  xpss12  5693  xpeq2  5699  elxpi  5700  elxp  5701  nfxp  5711  fconstmpt  5740  xpundi  5746  xpundir  5747  elopaelxp  5767  opabssxp  5770  csbxp  5777  ssrel  5784  ssrelOLD  5785  relopabiv  5822  relopabi  5824  inxpOLD  5835  dmxp  5931  resopab  6038  cnvxp  6161  xpco  6293  1st2val  8021  2nd2val  8022  dfxp3  8065  marypha2lem2  9460  wemapwe  9721  cardf2  9967  dfac3  10145  axdc2lem  10472  fpwwe2lem1  10655  canthwe  10675  xpcogend  14954  shftfval  15050  ipoval  18522  ipolerval  18524  eqgfval  19131  frgpuplem  19727  pjfval2  21643  ltbwe  21982  opsrtoslem1  21999  2ndcctbss  23372  ulmval  26329  lgsquadlem3  27328  iscgrg  28329  ishpg  28576  nvss  30416  ajfval  30632  fpwrelmap  32528  afsval  34303  cvmlift2lem12  34924  bj-opabssvv  36629  bj-xpcossxp  36668  dicval  40649  dnwech  42472  fgraphopab  42631  areaquad  42644  csbxpgVD  44333  relopabVD  44340  dfnelbr2  46653  xpsnopab  47219
  Copyright terms: Public domain W3C validator