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

Theorem relxp 5572
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 5570 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 5561 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 232 1 Rel (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3500  wss 3940   × cxp 5552  Rel wrel 5559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-in 3947  df-ss 3956  df-opab 5126  df-xp 5560  df-rel 5561
This theorem is referenced by:  xpsspw  5681  relinxp  5686  xpiindi  5705  eliunxp  5707  opeliunxp2  5708  relres  5881  restidsing  5921  codir  5978  qfto  5979  difxp  6019  sofld  6042  cnvcnv  6047  dfco2  6096  unixp  6131  ressn  6134  fliftcnv  7056  fliftfun  7057  oprssdm  7319  frxp  7811  opeliunxp2f  7867  reltpos  7888  tposfo  7910  tposf  7911  swoer  8309  xpider  8358  xpcomf1o  8595  fpwwe2lem9  10049  ordpinq  10354  addassnq  10369  mulassnq  10370  distrnq  10372  mulidnq  10374  recmulnq  10375  ltexnq  10386  prcdnq  10404  ltrel  10692  lerel  10694  dfle2  12530  fsumcom2  15119  fprodcom2  15328  0rest  16693  firest  16696  2oppchomf  16984  isinv  17020  invsym2  17023  invfun  17024  oppcsect2  17039  oppcinv  17040  oppchofcl  17500  oyoncl  17510  clatl  17716  gicer  18346  gsum2d2lem  19013  gsum2d2  19014  gsumcom2  19015  gsumxp  19016  dprd2d2  19086  mattpostpos  20979  mdetunilem9  21145  restbas  21682  txuni2  22089  txcls  22128  txdis1cn  22159  txkgen  22176  hmpher  22308  cnextrel  22587  tgphaus  22640  qustgplem  22644  tsmsxp  22678  utop2nei  22774  utop3cls  22775  xmeter  22958  caubl  23826  ovoliunlem1  24018  reldv  24383  taylf  24864  lgsquadlem1  25870  lgsquadlem2  25871  nvrel  28293  dfcnv2  30337  qusxpid  30842  qtophaus  30986  cvmliftlem1  32416  cvmlift2lem12  32445  gonan0  32523  dfso2  32874  relbigcup  33242  poimirlem3  34762  heicant  34794  vvdifopab  35389  dvhopellsm  38120  dibvalrel  38166  dib1dim  38168  diclspsn  38197  dih1  38289  dih1dimatlem  38332  aoprssdm  43267  eliunxp2  44214
  Copyright terms: Public domain W3C validator