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 5090
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 27181). Another example is that the set of rational numbers are defined in df-q 11749 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 5082 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1479 . . . . 5 class 𝑥
65, 1wcel 1987 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1479 . . . . 5 class 𝑦
98, 2wcel 1987 . . . 4 wff 𝑦𝐵
106, 9wa 384 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4682 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1480 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  xpeq1  5098  xpeq2  5099  elxpi  5100  elxp  5101  nfxp  5112  fconstmpt  5133  brab2a  5139  xpundi  5142  xpundir  5143  opabssxp  5164  csbxp  5171  ssrel  5178  xpss12  5196  relopabi  5215  inxp  5224  dmxp  5314  resopab  5415  cnvxp  5520  xpco  5644  1st2val  7154  2nd2val  7155  dfxp3  7190  marypha2lem2  8302  wemapwe  8554  cardf2  8729  dfac3  8904  axdc2lem  9230  fpwwe2lem1  9413  canthwe  9433  xpcogend  13663  shftfval  13760  ipoval  17094  ipolerval  17096  eqgfval  17582  frgpuplem  18125  ltbwe  19412  opsrtoslem1  19424  pjfval2  19993  2ndcctbss  21198  ulmval  24072  lgsquadlem3  25041  iscgrg  25341  ishpg  25585  nvss  27336  ajfval  27552  fpwrelmap  29392  afsval  30509  cvmlift2lem12  31057  dicval  35984  dnwech  37137  fgraphopab  37308  areaquad  37322  csbxpgOLD  38575  csbxpgVD  38652  relopabVD  38659  xpsnopab  41083
  Copyright terms: Public domain W3C validator