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  12996  fsumcom2  15595  fprodcom2  15803  0rest  17247  firest  17250  2oppchomf  17542  isinv  17579  invsym2  17582  invfun  17583  oppcsect2  17598  oppcinv  17599  oppchofcl  18085  oyoncl  18095  clatl  18333  gicer  19001  gsum2d2lem  19685  gsum2d2  19686  gsumcom2  19687  gsumxp  19688  dprd2d2  19758  mattpostpos  21731  mdetunilem9  21897  restbas  22437  txuni2  22844  txcls  22883  txdis1cn  22914  txkgen  22931  hmpher  23063  cnextrel  23342  tgphaus  23396  qustgplem  23400  tsmsxp  23434  utop2nei  23530  utop3cls  23531  xmeter  23714  caubl  24600  ovoliunlem1  24794  reldv  25162  taylf  25648  lgsquadlem1  26656  lgsquadlem2  26657  nvrel  29349  dfcnv2  31396  gsumpart  31698  qusxpid  31951  qtophaus  32197  cvmliftlem1  33659  cvmlift2lem12  33688  gonan0  33766  xpab  34079  dfso2  34122  frxp2  34183  frxp3  34189  relbigcup  34413  poimirlem3  36012  heicant  36044  vvdifopab  36651  cnvref4  36742  dvhopellsm  39511  dibvalrel  39557  dib1dim  39559  diclspsn  39588  dih1  39680  dih1dimatlem  39723  aoprssdm  45225  eliunxp2  46200  joindm2  46792  meetdm2  46794
  Copyright terms: Public domain W3C validator