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

Theorem relxp 4747
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 4746 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4641 . 2  |-  ( Rel  ( A  X.  B
)  <->  ( A  X.  B )  C_  ( _V  X.  _V ) )
31, 2mpbir 202 1  |-  Rel  ( A  X.  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2740    C_ wss 3094    X. cxp 4624   Rel wrel 4631
This theorem is referenced by:  xpsspwOLD  4751  xpiindi  4774  eliunxp  4776  opeliunxp2  4777  relres  4936  codir  5016  qfto  5017  sofld  5074  cnvcnv  5079  dfco2  5124  unixp  5157  ressn  5163  fliftcnv  5709  fliftfun  5710  oprssdm  5901  difxp  6052  frxp  6124  reltpos  6138  tpostpos  6153  tposfo  6160  tposf  6161  swoer  6621  xpider  6663  erinxp  6666  xpcomf1o  6884  cda1dif  7735  brdom3  8086  brdom5  8087  brdom4  8088  fpwwe2lem8  8192  fpwwe2lem9  8193  fpwwe2lem12  8196  ordpinq  8500  addassnq  8515  mulassnq  8516  distrnq  8518  mulidnq  8520  recmulnq  8521  ltexnq  8532  prcdnq  8550  ltrel  8820  lerel  8822  dfle2  10413  fsumcom2  12167  0rest  13261  firest  13264  pwsle  13318  2oppchomf  13554  isinv  13589  invsym2  13592  invfun  13593  oppcsect2  13604  oppcinv  13605  xpcbas  13879  oppchofcl  13961  oyoncl  13971  gicer  14667  gsum2d2lem  15151  gsum2d2  15152  gsumcom2  15153  gsumxp  15154  dprd2d2  15206  opsrtoslem2  16153  restbas  16816  txuni2  17187  txcls  17226  txdis1cn  17256  txkgen  17273  hmpher  17402  tgphaus  17726  divstgplem  17730  tsmsxp  17764  xmeter  17906  caubl  18660  ovoliunlem1  18788  reldv  19147  taylf  19667  lgsquadlem1  20520  lgsquadlem2  20521  nvrel  21083  cvmliftlem1  23153  cvmlift2lem12  23182  dfso2  23447  relbigcup  23778  restidsing  24407  prjcp1  24415  prjcp2  24416  cur1vald  24531  valcurfn1  24536  sqpre  24570  inposet  24610  limptlimpr2lem2  24907  dualalg  25114  dualded  25115  dvhopellsm  30437  dibvalrel  30483  dib1dim  30485  diclspsn  30514  dih1  30606  dih1dimatlem  30649
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-opab 4018  df-xp 4640  df-rel 4641
  Copyright terms: Public domain W3C validator