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 5409
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 28005). Another example is that the set of rational numbers are defined in df-q 12161 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 5401 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1506 . . . . 5 class 𝑥
65, 1wcel 2050 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1506 . . . . 5 class 𝑦
98, 2wcel 2050 . . . 4 wff 𝑦𝐵
106, 9wa 387 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4987 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1507 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5417  xpss12  5418  xpeq2  5424  elxpi  5425  elxp  5426  nfxp  5436  fconstmpt  5460  xpundi  5466  xpundir  5467  opabssxp  5489  csbxp  5496  ssrel  5503  relopabiv  5539  relopabi  5540  inxp  5549  dmxp  5639  resopab  5744  cnvxp  5851  xpco  5975  1st2val  7527  2nd2val  7528  dfxp3  7565  marypha2lem2  8693  wemapwe  8952  cardf2  9164  dfac3  9339  axdc2lem  9666  fpwwe2lem1  9849  canthwe  9869  xpcogend  14193  shftfval  14288  ipoval  17634  ipolerval  17636  eqgfval  18123  frgpuplem  18670  ltbwe  19978  opsrtoslem1  19989  pjfval2  20567  2ndcctbss  21779  ulmval  24683  lgsquadlem3  25672  iscgrg  26012  ishpg  26259  nvss  28159  ajfval  28375  fpwrelmap  30242  afsval  31619  cvmlift2lem12  32175  dicval  37786  dnwech  39073  fgraphopab  39235  areaquad  39248  csbxpgVD  40676  relopabVD  40683  dfnelbr2  42903  xpsnopab  43425
  Copyright terms: Public domain W3C validator