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

Theorem relxp 5649
Description: A Cartesian product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
relxp Rel (𝐴 × 𝐵)

Proof of Theorem relxp
StepHypRef Expression
1 xpss 5647 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 5638 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 230 1 Rel (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3444  wss 3909   × cxp 5629  Rel wrel 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-opab 5167  df-xp 5637  df-rel 5638
This theorem is referenced by:  xpsspw  5762  relinxp  5767  xpiindi  5788  eliunxp  5790  opeliunxp2  5791  relres  5963  restidsing  6003  codir  6071  qfto  6072  difxp  6113  sofld  6136  cnvcnv  6141  dfco2  6194  unixp  6231  ressn  6234  fliftcnv  7251  fliftfun  7252  oprssdm  7528  frxp  8047  opeliunxp2f  8109  reltpos  8130  tposfo  8152  tposf  8153  swoer  8612  xpider  8661  xpcomf1o  8939  fpwwe2lem8  10508  ordpinq  10813  addassnq  10828  mulassnq  10829  distrnq  10831  mulidnq  10833  recmulnq  10834  ltexnq  10845  prcdnq  10863  ltrel  11151  lerel  11153  dfle2  12995  fsumcom2  15594  fprodcom2  15802  0rest  17246  firest  17249  2oppchomf  17541  isinv  17578  invsym2  17581  invfun  17582  oppcsect2  17597  oppcinv  17598  oppchofcl  18084  oyoncl  18094  clatl  18332  gicer  18999  gsum2d2lem  19680  gsum2d2  19681  gsumcom2  19682  gsumxp  19683  dprd2d2  19753  mattpostpos  21726  mdetunilem9  21892  restbas  22432  txuni2  22839  txcls  22878  txdis1cn  22909  txkgen  22926  hmpher  23058  cnextrel  23337  tgphaus  23391  qustgplem  23395  tsmsxp  23429  utop2nei  23525  utop3cls  23526  xmeter  23709  caubl  24595  ovoliunlem1  24789  reldv  25157  taylf  25643  lgsquadlem1  26651  lgsquadlem2  26652  nvrel  29343  dfcnv2  31390  gsumpart  31692  qusxpid  31945  qtophaus  32191  cvmliftlem1  33653  cvmlift2lem12  33682  gonan0  33760  xpab  34073  dfso2  34119  frxp2  34180  frxp3  34186  relbigcup  34378  poimirlem3  35977  heicant  36009  vvdifopab  36616  cnvref4  36707  dvhopellsm  39476  dibvalrel  39522  dib1dim  39524  diclspsn  39553  dih1  39645  dih1dimatlem  39688  aoprssdm  45189  eliunxp2  46164  joindm2  46756  meetdm2  46758
  Copyright terms: Public domain W3C validator