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

Definition df-xp 4868
Description: Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ({1,5}X.{2,7})= (ex-xp 22765). Another example is that the set of rational numbers are defined in df-q 10818 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 4860 . 2
4 vx . . . . . 6
54cv 1669 . . . . 5
65, 1wcel 1732 . . . 4
7 vy . . . . . 6
87cv 1669 . . . . 5
98, 2wcel 1732 . . . 4
106, 9wa 360 . . 3
1110, 4, 7copab 4375 . 2
123, 11wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4876  xpeq2  4877  elxpi  4878  elxp  4879  nfxp  4888  fconstmpt  4904  brab2a  4910  xpundi  4913  xpundir  4914  opabssxp  4933  csbxp  4940  csbxpgOLD  4941  xpss12  4967  inxp  4994  dmxp  5080  resopab  5176  cnvxp  5277  xpco  5397  1st2val  6608  2nd2val  6609  dfxp3  6640  marypha2lem2  7608  wemapwe  7821  cardf2  7999  dfac3  8173  axdc2lem  8499  fpwwe2lem1  8677  canthwe  8697  shftfval  12406  ipoval  15165  ipolerval  15167  eqgfval  15559  frgpuplem  16013  ltbwe  17158  opsrtoslem1  17169  pjfval2  17561  2ndcctbss  18533  ulmval  21311  lgsquadlem3  22161  iseupa  22708  nvss  23093  ajfval  23331  fpwrelmap  25163  cvmlift2lem12  26349  dnwech  28549  fgraphopab  28760  csbxpgVD  30476  relopabVD  30483  dicval  33524
  Copyright terms: Public domain W3C validator