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 5317
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 27620). Another example is that the set of rational numbers are defined in df-q 12004 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 5309 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1636 . . . . 5 class 𝑥
65, 1wcel 2156 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1636 . . . . 5 class 𝑦
98, 2wcel 2156 . . . 4 wff 𝑦𝐵
106, 9wa 384 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4906 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1637 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5325  xpss12  5326  xpeq2  5331  elxpi  5332  elxp  5333  nfxp  5343  fconstmpt  5363  xpundi  5371  xpundir  5372  opabssxp  5395  csbxp  5402  ssrel  5409  relopabi  5447  inxp  5456  dmxp  5545  resopab  5651  cnvxp  5762  xpco  5889  1st2val  7422  2nd2val  7423  dfxp3  7459  marypha2lem2  8577  wemapwe  8837  cardf2  9048  dfac3  9223  axdc2lem  9551  fpwwe2lem1  9734  canthwe  9754  xpcogend  13934  shftfval  14029  ipoval  17355  ipolerval  17357  eqgfval  17840  frgpuplem  18382  ltbwe  19677  opsrtoslem1  19688  pjfval2  20259  2ndcctbss  21468  ulmval  24344  lgsquadlem3  25317  iscgrg  25617  ishpg  25861  nvss  27772  ajfval  27988  fpwrelmap  29831  afsval  31070  cvmlift2lem12  31614  dicval  36951  dnwech  38113  fgraphopab  38283  areaquad  38296  csbxpgOLD  39542  csbxpgVD  39618  relopabVD  39625  dfnelbr2  41856  xpsnopab  42327
  Copyright terms: Public domain W3C validator