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

Theorem relxp 4701
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 4700 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4595 . 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 2727    C_ wss 3078    X. cxp 4578   Rel wrel 4585
This theorem is referenced by:  xpsspwOLD  4705  xpiindi  4728  eliunxp  4730  opeliunxp2  4731  relres  4890  codir  4970  qfto  4971  sofld  5028  cnvcnv  5033  dfco2  5078  unixp  5111  ressn  5117  fliftcnv  5662  fliftfun  5663  oprssdm  5854  difxp  6005  frxp  6077  reltpos  6091  tpostpos  6106  tposfo  6113  tposf  6114  swoer  6574  xpider  6616  erinxp  6619  xpcomf1o  6836  cda1dif  7686  brdom3  8037  brdom5  8038  brdom4  8039  fpwwe2lem8  8139  fpwwe2lem9  8140  fpwwe2lem12  8143  ordpinq  8447  addassnq  8462  mulassnq  8463  distrnq  8465  mulidnq  8467  recmulnq  8468  ltexnq  8479  prcdnq  8497  ltrel  8767  lerel  8769  dfle2  10360  fsumcom2  12114  0rest  13208  firest  13211  pwsle  13265  2oppchomf  13471  isinv  13506  invsym2  13509  invfun  13510  oppcsect2  13521  oppcinv  13522  xpcbas  13796  oppchofcl  13878  oyoncl  13888  gicer  14575  gsum2d2lem  15059  gsum2d2  15060  gsumcom2  15061  gsumxp  15062  dprd2d2  15114  opsrtoslem2  16058  restbas  16721  txuni2  17092  txcls  17131  txdis1cn  17161  txkgen  17178  hmpher  17307  tgphaus  17631  divstgplem  17635  tsmsxp  17669  xmeter  17811  caubl  18565  ovoliunlem1  18693  reldv  19052  taylf  19572  lgsquadlem1  20425  lgsquadlem2  20426  nvrel  20988  cvmliftlem1  22987  cvmlift2lem12  23016  dfso2  23281  relbigcup  23612  restidsing  24241  prjcp1  24249  prjcp2  24250  cur1vald  24365  valcurfn1  24370  sqpre  24404  inposet  24444  limptlimpr2lem2  24741  dualalg  24948  dualded  24949  dvhopellsm  29996  dibvalrel  30042  dib1dim  30044  diclspsn  30073  dih1  30165  dih1dimatlem  30208
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-opab 3975  df-xp 4594  df-rel 4595
  Copyright terms: Public domain W3C validator