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

Theorem relxp 4969
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 4968 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4871 . 2  |-  ( Rel  ( A  X.  B
)  <->  ( A  X.  B )  C_  ( _V  X.  _V ) )
31, 2mpbir 201 1  |-  Rel  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2943    C_ wss 3307    X. cxp 4862   Rel wrel 4869
This theorem is referenced by:  xpsspwOLD  4973  xpiindi  4996  eliunxp  4998  opeliunxp2  4999  relres  5160  codir  5240  qfto  5241  sofld  5304  cnvcnv  5309  dfco2  5355  unixp  5388  ressn  5394  fliftcnv  6019  fliftfun  6020  oprssdm  6214  difxp  6366  frxp  6442  reltpos  6470  tpostpos  6485  tposfo  6492  tposf  6493  swoer  6919  xpider  6961  erinxp  6964  xpcomf1o  7183  cda1dif  8040  brdom3  8390  brdom5  8391  brdom4  8392  fpwwe2lem8  8496  fpwwe2lem9  8497  fpwwe2lem12  8500  ordpinq  8804  addassnq  8819  mulassnq  8820  distrnq  8822  mulidnq  8824  recmulnq  8825  ltexnq  8836  prcdnq  8854  ltrel  9124  lerel  9126  dfle2  10724  fsumcom2  12541  0rest  13640  firest  13643  pwsle  13697  2oppchomf  13933  isinv  13968  invsym2  13971  invfun  13972  oppcsect2  13983  oppcinv  13984  oppchofcl  14340  oyoncl  14350  gicer  15046  gsum2d2lem  15530  gsum2d2  15531  gsumcom2  15532  gsumxp  15533  dprd2d2  15585  opsrtoslem2  16528  restbas  17205  txuni2  17580  txcls  17619  txdis1cn  17650  txkgen  17667  hmpher  17799  cnextrel  18077  tgphaus  18129  divstgplem  18133  tsmsxp  18167  utop2nei  18263  utop3cls  18264  xmeter  18446  caubl  19243  ovoliunlem1  19381  reldv  19740  taylf  20260  lgsquadlem1  21121  lgsquadlem2  21122  nvrel  22064  cvmliftlem1  24955  cvmlift2lem12  24984  fprodcom2  25292  dfso2  25361  elrn3  25370  relbigcup  25687  aoprssdm  27975  dvhopellsm  31646  dibvalrel  31692  dib1dim  31694  diclspsn  31723  dih1  31815  dih1dimatlem  31858
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-in 3314  df-ss 3321  df-opab 4254  df-xp 4870  df-rel 4871
  Copyright terms: Public domain W3C validator