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

Definition df-xp 4850
Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ({1,5}X.{2,7})= (ex-xp 22253). Another example is that the set of rational numbers are defined in df-q 10761 using the cross-product ; the left- and right-hand sides of the cross-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 4842 . 2
4 vx . . . . . 6
54cv 1661 . . . . 5
65, 1wcel 1724 . . . 4
7 vy . . . . . 6
87cv 1661 . . . . 5
98, 2wcel 1724 . . . 4
106, 9wa 360 . . 3
1110, 4, 7copab 4359 . 2
123, 11wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4858  xpeq2  4859  elxpi  4860  elxp  4861  nfxp  4870  fconstmpt  4886  brab2a  4892  xpundi  4895  xpundir  4896  opabssxp  4915  csbxp  4922  csbxpgOLD  4923  xpss12  4949  inxp  4976  dmxp  5062  resopab  5156  cnvxp  5256  xpco  5376  1st2val  6563  2nd2val  6564  dfxp3  6595  marypha2lem2  7553  wemapwe  7766  cardf2  7944  dfac3  8116  axdc2lem  8442  fpwwe2lem1  8620  canthwe  8640  shftfval  12345  ipoval  15102  ipolerval  15104  eqgfval  15491  frgpuplem  15907  ltbwe  17036  opsrtoslem1  17047  pjfval2  17439  2ndcctbss  18022  ulmval  20800  lgsquadlem3  21649  iseupa  22196  nvss  22581  ajfval  22819  fpwrelmap  24654  cvmlift2lem12  25840  dnwech  28052  fgraphopab  28435  csbxpgVD  30199  relopabVD  30206  dicval  33247
  Copyright terms: Public domain W3C validator