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

Definition df-xp 4925
Description: Define the cross product of two classes. Definition 9.11 of [Quine] ?Error: 1 , 5 } X. { 2 , 7 } ) = ^ This math symbol is not active (i.e. was not declared in this scope). p. 64. For example, ({1,5}X.{2,7})= ?Error: 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ) ^ This math symbol is not active (i.e. was not declared in this scope). ({<.1,2>.,<.1,7>.}u.{<.5,2>.,<.5,7>.}) (ex-xp 21795). Another example is that the set of rational numbers are ?Error: ZZ X. NN ) ^^ This math symbol is not active (i.e. was not declared in this scope). defined in df-q 10626 using the cross-product ( X. ); 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 4917 . 2
4 vx . . . . . 6
54cv 1653 . . . . 5
65, 1wcel 1728 . . . 4
7 vy . . . . . 6
87cv 1653 . . . . 5
98, 2wcel 1728 . . . 4
106, 9wa 360 . . 3
1110, 4, 7copab 4300 . 2
123, 11wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  xpeq1  4933  xpeq2  4934  elxpi  4935  elxp  4936  nfxp  4945  fconstmpt  4961  brab2a  4967  xpundi  4970  xpundir  4971  opabssxp  4990  csbxp  4997  csbxpgOLD  4998  xpss12  5023  inxp  5049  dmxp  5132  resopab  5231  cnvxp  5334  xpco  5460  1st2val  6422  2nd2val  6423  dfxp3  6456  marypha2lem2  7490  wemapwe  7703  cardf2  7881  dfac3  8053  axdc2lem  8379  fpwwe2lem1  8557  canthwe  8577  shftfval  11936  ipoval  14631  ipolerval  14633  eqgfval  15039  frgpuplem  15455  ltbwe  16584  opsrtoslem1  16595  pjfval2  16987  2ndcctbss  17569  ulmval  20347  lgsquadlem3  21191  iseupa  21738  nvss  22123  ajfval  22361  fpwrelmap  24737  cvmlift2lem12  25105  dnwech  27302  fgraphopab  27685  csbxpgVD  29247  relopabVD  29254  dicval  32214
  Copyright terms: Public domain W3C validator