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

Theorem relxp 5294
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 5292 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 5283 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 222 1 Rel (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3349  wss 3731   × cxp 5274  Rel wrel 5281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-in 3738  df-ss 3745  df-opab 4871  df-xp 5282  df-rel 5283
This theorem is referenced by:  xpsspw  5400  relinxp  5405  xpiindi  5425  eliunxp  5427  opeliunxp2  5428  relres  5600  restidsing  5641  codir  5698  qfto  5699  difxp  5740  sofld  5763  cnvcnv  5768  cnvcnvOLD  5769  dfco2  5819  unixp  5853  ressn  5856  fliftcnv  6752  fliftfun  6753  oprssdm  7012  frxp  7488  opeliunxp2f  7538  reltpos  7559  tpostpos  7574  tposfo  7581  tposf  7582  swoer  7976  xpider  8020  xpcomf1o  8255  cda1dif  9250  brdom3  9602  brdom5  9603  brdom4  9604  fpwwe2lem9  9712  ordpinq  10017  addassnq  10032  mulassnq  10033  distrnq  10035  mulidnq  10037  recmulnq  10038  ltexnq  10049  prcdnq  10067  ltrel  10353  lerel  10355  dfle2  12179  fsumcom2  14791  fprodcom2  14998  0rest  16357  firest  16360  2oppchomf  16650  isinv  16686  invsym2  16689  invfun  16690  oppcsect2  16705  oppcinv  16706  oppchofcl  17167  oyoncl  17177  clatl  17383  gicer  17983  gsum2d2lem  18637  gsum2d2  18638  gsumcom2  18639  gsumxp  18640  dprd2d2  18709  opsrtoslem2  19757  mattpostpos  20536  mdetunilem9  20702  restbas  21241  txuni2  21647  txcls  21686  txdis1cn  21717  txkgen  21734  hmpher  21866  cnextrel  22145  tgphaus  22198  qustgplem  22202  tsmsxp  22236  utop2nei  22332  utop3cls  22333  xmeter  22516  caubl  23384  ovoliunlem1  23559  reldv  23924  taylf  24405  lgsquadlem1  25395  lgsquadlem2  25396  nvrel  27847  dfcnv2  29859  qtophaus  30284  cvmliftlem1  31646  cvmlift2lem12  31675  dfso2  32020  elrn3  32028  relbigcup  32379  poimirlem3  33768  heicant  33800  vvdifopab  34391  inxprnres  34424  dvhopellsm  37005  dibvalrel  37051  dib1dim  37053  diclspsn  37082  dih1  37174  dih1dimatlem  37217  aoprssdm  41882  eliunxp2  42713
  Copyright terms: Public domain W3C validator