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

Theorem relxp 4794
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 4793 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4696 . 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 2788    C_ wss 3152    X. cxp 4687   Rel wrel 4694
This theorem is referenced by:  xpsspwOLD  4798  xpiindi  4821  eliunxp  4823  opeliunxp2  4824  relres  4983  codir  5063  qfto  5064  sofld  5121  cnvcnv  5126  dfco2  5172  unixp  5205  ressn  5211  fliftcnv  5810  fliftfun  5811  oprssdm  6002  difxp  6153  frxp  6225  reltpos  6239  tpostpos  6254  tposfo  6261  tposf  6262  swoer  6688  xpider  6730  erinxp  6733  xpcomf1o  6951  cda1dif  7802  brdom3  8153  brdom5  8154  brdom4  8155  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  ordpinq  8567  addassnq  8582  mulassnq  8583  distrnq  8585  mulidnq  8587  recmulnq  8588  ltexnq  8599  prcdnq  8617  ltrel  8887  lerel  8889  dfle2  10481  fsumcom2  12237  0rest  13334  firest  13337  pwsle  13391  2oppchomf  13627  isinv  13662  invsym2  13665  invfun  13666  oppcsect2  13677  oppcinv  13678  xpcbas  13952  oppchofcl  14034  oyoncl  14044  gicer  14740  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  gsumxp  15227  dprd2d2  15279  opsrtoslem2  16226  restbas  16889  txuni2  17260  txcls  17299  txdis1cn  17329  txkgen  17346  hmpher  17475  tgphaus  17799  divstgplem  17803  tsmsxp  17837  xmeter  17979  caubl  18733  ovoliunlem1  18861  reldv  19220  taylf  19740  lgsquadlem1  20593  lgsquadlem2  20594  nvrel  21158  cvmliftlem1  23816  cvmlift2lem12  23845  dfso2  24111  elrn3  24120  relbigcup  24437  restidsing  25076  prjcp1  25084  prjcp2  25085  cur1vald  25199  valcurfn1  25204  sqpre  25238  inposet  25278  limptlimpr2lem2  25575  dualalg  25782  dualded  25783  aoprssdm  28062  dvhopellsm  31307  dibvalrel  31353  dib1dim  31355  diclspsn  31384  dih1  31476  dih1dimatlem  31519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-opab 4078  df-xp 4695  df-rel 4696
  Copyright terms: Public domain W3C validator