Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xp Structured version   Visualization version   GIF version

Definition df-xp 5044
 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 26685). Another example is that the set of rational numbers are defined in df-q 11665 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 5036 . 2 class (𝐴 × 𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1474 . . . . 5 class 𝑥
65, 1wcel 1977 . . . 4 wff 𝑥𝐴
7 vy . . . . . 6 setvar 𝑦
87cv 1474 . . . . 5 class 𝑦
98, 2wcel 1977 . . . 4 wff 𝑦𝐵
106, 9wa 383 . . 3 wff (𝑥𝐴𝑦𝐵)
1110, 4, 7copab 4642 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
123, 11wceq 1475 1 wff (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
 Colors of variables: wff setvar class This definition is referenced by:  xpeq1  5052  xpeq2  5053  elxpi  5054  elxp  5055  nfxp  5066  fconstmpt  5085  brab2a  5091  xpundi  5094  xpundir  5095  opabssxp  5116  csbxp  5123  ssrel  5130  xpss12  5148  relopabi  5167  inxp  5176  dmxp  5265  resopab  5366  cnvxp  5470  xpco  5592  1st2val  7085  2nd2val  7086  dfxp3  7119  marypha2lem2  8225  wemapwe  8477  cardf2  8652  dfac3  8827  axdc2lem  9153  fpwwe2lem1  9332  canthwe  9352  xpcogend  13561  shftfval  13658  ipoval  16977  ipolerval  16979  eqgfval  17465  frgpuplem  18008  ltbwe  19293  opsrtoslem1  19305  pjfval2  19872  2ndcctbss  21068  ulmval  23938  lgsquadlem3  24907  iscgrg  25207  ishpg  25451  iseupa  26492  nvss  26832  ajfval  27048  fpwrelmap  28896  afsval  30002  cvmlift2lem12  30550  dicval  35483  dnwech  36636  fgraphopab  36807  areaquad  36821  csbxpgOLD  38075  csbxpgVD  38152  relopabVD  38159  xpsnopab  41555
 Copyright terms: Public domain W3C validator