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 5555
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 28143). Another example is that the set of rational numbers are defined in df-q 12338 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 5547 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1527 . . . . 5 class 𝑥
65, 1wcel 2105 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1527 . . . . 5 class 𝑦
98, 2wcel 2105 . . . 4 wff 𝑦𝐵
106, 9wa 396 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 5120 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1528 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5563  xpss12  5564  xpeq2  5570  elxpi  5571  elxp  5572  nfxp  5582  fconstmpt  5608  xpundi  5614  xpundir  5615  opabssxp  5637  csbxp  5644  ssrel  5651  relopabiv  5687  relopabi  5688  inxp  5697  dmxp  5793  resopab  5896  cnvxp  6008  xpco  6134  1st2val  7708  2nd2val  7709  dfxp3  7750  marypha2lem2  8889  wemapwe  9149  cardf2  9361  dfac3  9536  axdc2lem  9859  fpwwe2lem1  10042  canthwe  10062  xpcogend  14324  shftfval  14419  ipoval  17754  ipolerval  17756  eqgfval  18268  frgpuplem  18829  ltbwe  20183  opsrtoslem1  20194  pjfval2  20783  2ndcctbss  21993  ulmval  24897  lgsquadlem3  25886  iscgrg  26226  ishpg  26473  nvss  28298  ajfval  28514  fpwrelmap  30396  afsval  31842  cvmlift2lem12  32459  bj-opabssvv  34335  dicval  38194  dnwech  39528  fgraphopab  39690  areaquad  39703  csbxpgVD  41108  relopabVD  41115  dfnelbr2  43353  xpsnopab  43879
  Copyright terms: Public domain W3C validator