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

Theorem relxp 4793
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 4792 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4695 . 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 2789    C_ wss 3153    X. cxp 4686   Rel wrel 4693
This theorem is referenced by:  xpsspwOLD  4797  xpiindi  4820  eliunxp  4822  opeliunxp2  4823  relres  4982  codir  5062  qfto  5063  sofld  5120  cnvcnv  5125  dfco2  5170  unixp  5203  ressn  5209  fliftcnv  5771  fliftfun  5772  oprssdm  5963  difxp  6114  frxp  6186  reltpos  6200  tpostpos  6215  tposfo  6222  tposf  6223  swoer  6683  xpider  6725  erinxp  6728  xpcomf1o  6946  cda1dif  7797  brdom3  8148  brdom5  8149  brdom4  8150  fpwwe2lem8  8254  fpwwe2lem9  8255  fpwwe2lem12  8258  ordpinq  8562  addassnq  8577  mulassnq  8578  distrnq  8580  mulidnq  8582  recmulnq  8583  ltexnq  8594  prcdnq  8612  ltrel  8882  lerel  8884  dfle2  10476  fsumcom2  12231  0rest  13328  firest  13331  pwsle  13385  2oppchomf  13621  isinv  13656  invsym2  13659  invfun  13660  oppcsect2  13671  oppcinv  13672  xpcbas  13946  oppchofcl  14028  oyoncl  14038  gicer  14734  gsum2d2lem  15218  gsum2d2  15219  gsumcom2  15220  gsumxp  15221  dprd2d2  15273  opsrtoslem2  16220  restbas  16883  txuni2  17254  txcls  17293  txdis1cn  17323  txkgen  17340  hmpher  17469  tgphaus  17793  divstgplem  17797  tsmsxp  17831  xmeter  17973  caubl  18727  ovoliunlem1  18855  reldv  19214  taylf  19734  lgsquadlem1  20587  lgsquadlem2  20588  nvrel  21150  cvmliftlem1  23220  cvmlift2lem12  23249  dfso2  23514  relbigcup  23845  restidsing  24474  prjcp1  24482  prjcp2  24483  cur1vald  24598  valcurfn1  24603  sqpre  24637  inposet  24677  limptlimpr2lem2  24974  dualalg  25181  dualded  25182  aoprssdm  27441  dvhopellsm  30574  dibvalrel  30620  dib1dim  30622  diclspsn  30651  dih1  30743  dih1dimatlem  30786
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-opab 4079  df-xp 4694  df-rel 4695
  Copyright terms: Public domain W3C validator