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

Definition df-xp 5010
 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}X.{2,7})= (ex-xp 25157). Another example is that the set of rational numbers are defined in df-q 11212 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
2 cB . . 3
31, 2cxp 5002 . 2
4 vx . . . . . 6
54cv 1394 . . . . 5
65, 1wcel 1818 . . . 4
7 vy . . . . . 6
87cv 1394 . . . . 5
98, 2wcel 1818 . . . 4
106, 9wa 369 . . 3
1110, 4, 7copab 4509 . 2
123, 11wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  xpeq1  5018  xpeq2  5019  elxpi  5020  elxp  5021  nfxp  5031  fconstmpt  5048  brab2a  5054  xpundi  5057  xpundir  5058  opabssxp  5079  csbxp  5086  csbxpgOLD  5087  xpss12  5113  inxp  5140  dmxp  5226  resopab  5325  cnvxp  5429  xpco  5552  1st2val  6826  2nd2val  6827  dfxp3  6860  marypha2lem2  7916  wemapwe  8160  wemapweOLD  8161  cardf2  8345  dfac3  8523  axdc2lem  8849  fpwwe2lem1  9030  canthwe  9050  shftfval  12903  ipoval  15784  ipolerval  15786  eqgfval  16249  frgpuplem  16790  ltbwe  18137  opsrtoslem1  18148  pjfval2  18740  2ndcctbss  19956  ulmval  22775  lgsquadlem3  23631  iscgrg  23904  ishpg  24128  iseupa  24965  nvss  25486  ajfval  25724  fpwrelmap  27556  afsval  28551  cvmlift2lem12  28759  dnwech  30994  fgraphopab  31170  areaquad  31184  xpsnopab  32453  csbxpgVD  33694  relopabVD  33701  dicval  36903  xpcogend  37773
 Copyright terms: Public domain W3C validator