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

Theorem relxp 4768
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 4767 . 2  |-  ( A  X.  B )  C_  ( _V  X.  _V )
2 df-rel 4662 . 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 2757    C_ wss 3113    X. cxp 4645   Rel wrel 4652
This theorem is referenced by:  xpsspwOLD  4772  xpiindi  4795  eliunxp  4797  opeliunxp2  4798  relres  4957  codir  5037  qfto  5038  sofld  5095  cnvcnv  5100  dfco2  5145  unixp  5178  ressn  5184  fliftcnv  5730  fliftfun  5731  oprssdm  5922  difxp  6073  frxp  6145  reltpos  6159  tpostpos  6174  tposfo  6181  tposf  6182  swoer  6642  xpider  6684  erinxp  6687  xpcomf1o  6905  cda1dif  7756  brdom3  8107  brdom5  8108  brdom4  8109  fpwwe2lem8  8213  fpwwe2lem9  8214  fpwwe2lem12  8217  ordpinq  8521  addassnq  8536  mulassnq  8537  distrnq  8539  mulidnq  8541  recmulnq  8542  ltexnq  8553  prcdnq  8571  ltrel  8841  lerel  8843  dfle2  10434  fsumcom2  12188  0rest  13282  firest  13285  pwsle  13339  2oppchomf  13575  isinv  13610  invsym2  13613  invfun  13614  oppcsect2  13625  oppcinv  13626  xpcbas  13900  oppchofcl  13982  oyoncl  13992  gicer  14688  gsum2d2lem  15172  gsum2d2  15173  gsumcom2  15174  gsumxp  15175  dprd2d2  15227  opsrtoslem2  16174  restbas  16837  txuni2  17208  txcls  17247  txdis1cn  17277  txkgen  17294  hmpher  17423  tgphaus  17747  divstgplem  17751  tsmsxp  17785  xmeter  17927  caubl  18681  ovoliunlem1  18809  reldv  19168  taylf  19688  lgsquadlem1  20541  lgsquadlem2  20542  nvrel  21104  cvmliftlem1  23174  cvmlift2lem12  23203  dfso2  23468  relbigcup  23799  restidsing  24428  prjcp1  24436  prjcp2  24437  cur1vald  24552  valcurfn1  24557  sqpre  24591  inposet  24631  limptlimpr2lem2  24928  dualalg  25135  dualded  25136  dvhopellsm  30458  dibvalrel  30504  dib1dim  30506  diclspsn  30535  dih1  30627  dih1dimatlem  30670
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 2759  df-in 3120  df-ss 3127  df-opab 4038  df-xp 4661  df-rel 4662
  Copyright terms: Public domain W3C validator