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 5033
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 26478). Another example is that the set of rational numbers are defined in df-q 11623 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 5025 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1473 . . . . 5 class 𝑥
65, 1wcel 1976 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1473 . . . . 5 class 𝑦
98, 2wcel 1976 . . . 4 wff 𝑦𝐵
106, 9wa 382 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4636 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1474 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5041  xpeq2  5042  elxpi  5043  elxp  5044  nfxp  5055  fconstmpt  5074  brab2a  5080  xpundi  5083  xpundir  5084  opabssxp  5105  csbxp  5112  xpss12  5136  inxp  5163  dmxp  5251  resopab  5352  cnvxp  5455  xpco  5577  1st2val  7062  2nd2val  7063  dfxp3  7096  marypha2lem2  8202  wemapwe  8454  cardf2  8629  dfac3  8804  axdc2lem  9130  fpwwe2lem1  9309  canthwe  9329  xpcogend  13509  shftfval  13606  ipoval  16925  ipolerval  16927  eqgfval  17413  frgpuplem  17956  ltbwe  19241  opsrtoslem1  19253  pjfval2  19819  2ndcctbss  21015  ulmval  23882  lgsquadlem3  24851  iscgrg  25152  ishpg  25396  iseupa  26285  nvss  26625  ajfval  26841  fpwrelmap  28689  afsval  29795  cvmlift2lem12  30343  dicval  35266  dnwech  36419  fgraphopab  36590  areaquad  36604  csbxpgOLD  37858  csbxpgVD  37935  relopabVD  37942  xpsnopab  41536
  Copyright terms: Public domain W3C validator