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 5149
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 27423). Another example is that the set of rational numbers are defined in df-q 11827 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 5141 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1522 . . . . 5 class 𝑥
65, 1wcel 2030 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1522 . . . . 5 class 𝑦
98, 2wcel 2030 . . . 4 wff 𝑦𝐵
106, 9wa 383 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4745 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1523 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5157  xpss12  5158  xpeq2  5163  elxpi  5164  elxp  5165  nfxp  5176  fconstmpt  5197  xpundi  5205  xpundir  5206  opabssxp  5227  csbxp  5234  ssrel  5241  relopabi  5278  inxp  5287  dmxp  5376  resopab  5481  cnvxp  5586  xpco  5713  1st2val  7238  2nd2val  7239  dfxp3  7275  marypha2lem2  8383  wemapwe  8632  cardf2  8807  dfac3  8982  axdc2lem  9308  fpwwe2lem1  9491  canthwe  9511  xpcogend  13759  shftfval  13854  ipoval  17201  ipolerval  17203  eqgfval  17689  frgpuplem  18231  ltbwe  19520  opsrtoslem1  19532  pjfval2  20101  2ndcctbss  21306  ulmval  24179  lgsquadlem3  25152  iscgrg  25452  ishpg  25696  nvss  27576  ajfval  27792  fpwrelmap  29636  afsval  30877  cvmlift2lem12  31422  dicval  36782  dnwech  37935  fgraphopab  38105  areaquad  38119  csbxpgOLD  39368  csbxpgVD  39444  relopabVD  39451  dfnelbr2  41614  xpsnopab  42090
  Copyright terms: Public domain W3C validator