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

Theorem relxp 4810
Description: A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
relxp  |-  Rel  ( A  X.  B )

Proof of Theorem relxp
StepHypRef Expression
1 xpss 4809 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4712 . 2  |-  ( Rel  ( A  X.  B
)  <->  ( A  X.  B )  C_  ( _V  X.  _V ) )
31, 2mpbir 200 1  |-  Rel  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2801    C_ wss 3165    X. cxp 4703   Rel wrel 4710
This theorem is referenced by:  xpsspwOLD  4814  xpiindi  4837  eliunxp  4839  opeliunxp2  4840  relres  4999  codir  5079  qfto  5080  sofld  5137  cnvcnv  5142  dfco2  5188  unixp  5221  ressn  5227  fliftcnv  5826  fliftfun  5827  oprssdm  6018  difxp  6169  frxp  6241  reltpos  6255  tpostpos  6270  tposfo  6277  tposf  6278  swoer  6704  xpider  6746  erinxp  6749  xpcomf1o  6967  cda1dif  7818  brdom3  8169  brdom5  8170  brdom4  8171  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  ordpinq  8583  addassnq  8598  mulassnq  8599  distrnq  8601  mulidnq  8603  recmulnq  8604  ltexnq  8615  prcdnq  8633  ltrel  8903  lerel  8905  dfle2  10497  fsumcom2  12253  0rest  13350  firest  13353  pwsle  13407  2oppchomf  13643  isinv  13678  invsym2  13681  invfun  13682  oppcsect2  13693  oppcinv  13694  xpcbas  13968  oppchofcl  14050  oyoncl  14060  gicer  14756  gsum2d2lem  15240  gsum2d2  15241  gsumcom2  15242  gsumxp  15243  dprd2d2  15295  opsrtoslem2  16242  restbas  16905  txuni2  17276  txcls  17315  txdis1cn  17345  txkgen  17362  hmpher  17491  tgphaus  17815  divstgplem  17819  tsmsxp  17853  xmeter  17995  caubl  18749  ovoliunlem1  18877  reldv  19236  taylf  19756  lgsquadlem1  20609  lgsquadlem2  20610  nvrel  21174  cvmliftlem1  23831  cvmlift2lem12  23860  dfso2  24182  elrn3  24191  relbigcup  24508  restidsing  25179  prjcp1  25187  prjcp2  25188  cur1vald  25302  valcurfn1  25307  sqpre  25341  inposet  25381  limptlimpr2lem2  25678  dualalg  25885  dualded  25886  aoprssdm  28170  dvhopellsm  31929  dibvalrel  31975  dib1dim  31977  diclspsn  32006  dih1  32098  dih1dimatlem  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-opab 4094  df-xp 4711  df-rel 4712
  Copyright terms: Public domain W3C validator