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 5549
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 28230). Another example is that the set of rational numbers are defined in df-q 12348 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 5541 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1537 . . . . 5 class 𝑥
65, 1wcel 2115 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1537 . . . . 5 class 𝑦
98, 2wcel 2115 . . . 4 wff 𝑦𝐵
106, 9wa 399 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 5115 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1538 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5557  xpss12  5558  xpeq2  5564  elxpi  5565  elxp  5566  nfxp  5576  fconstmpt  5602  xpundi  5608  xpundir  5609  opabssxp  5631  csbxp  5638  ssrel  5645  relopabiv  5681  relopabi  5682  inxp  5691  dmxp  5787  resopab  5891  cnvxp  6003  xpco  6129  1st2val  7714  2nd2val  7715  dfxp3  7756  marypha2lem2  8899  wemapwe  9159  cardf2  9371  dfac3  9547  axdc2lem  9870  fpwwe2lem1  10053  canthwe  10073  xpcogend  14336  shftfval  14431  ipoval  17766  ipolerval  17768  eqgfval  18330  frgpuplem  18900  pjfval2  20407  ltbwe  20721  opsrtoslem1  20732  2ndcctbss  22069  ulmval  24984  lgsquadlem3  25975  iscgrg  26315  ishpg  26562  nvss  28385  ajfval  28601  fpwrelmap  30490  afsval  32027  cvmlift2lem12  32646  bj-opabssvv  34537  bj-xpcossxp  34576  dicval  38444  dnwech  39936  fgraphopab  40098  areaquad  40110  csbxpgVD  41548  relopabVD  41555  dfnelbr2  43782  xpsnopab  44338
  Copyright terms: Public domain W3C validator