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 5264
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 27596). Another example is that the set of rational numbers are defined in df-q 11974 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 5256 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1623 . . . . 5 class 𝑥
65, 1wcel 2131 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1623 . . . . 5 class 𝑦
98, 2wcel 2131 . . . 4 wff 𝑦𝐵
106, 9wa 383 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4856 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1624 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5272  xpss12  5273  xpeq2  5278  elxpi  5279  elxp  5280  nfxp  5291  fconstmpt  5312  xpundi  5320  xpundir  5321  opabssxp  5342  csbxp  5349  ssrel  5356  relopabi  5393  inxp  5402  dmxp  5491  resopab  5596  cnvxp  5701  xpco  5828  1st2val  7353  2nd2val  7354  dfxp3  7390  marypha2lem2  8499  wemapwe  8759  cardf2  8951  dfac3  9126  axdc2lem  9454  fpwwe2lem1  9637  canthwe  9657  xpcogend  13906  shftfval  14001  ipoval  17347  ipolerval  17349  eqgfval  17835  frgpuplem  18377  ltbwe  19666  opsrtoslem1  19678  pjfval2  20247  2ndcctbss  21452  ulmval  24325  lgsquadlem3  25298  iscgrg  25598  ishpg  25842  nvss  27749  ajfval  27965  fpwrelmap  29809  afsval  31050  cvmlift2lem12  31595  dicval  36959  dnwech  38112  fgraphopab  38282  areaquad  38296  csbxpgOLD  39545  csbxpgVD  39621  relopabVD  39628  dfnelbr2  41791  xpsnopab  42267
  Copyright terms: Public domain W3C validator