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

Theorem relxp 5150
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 5149 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 5045 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 220 1 Rel (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3173  wss 3540   × cxp 5036  Rel wrel 5043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-rel 5045
This theorem is referenced by:  xpsspw  5156  xpiindi  5179  eliunxp  5181  opeliunxp2  5182  relres  5346  restidsing  5377  restidsingOLD  5378  codir  5435  qfto  5436  difxp  5477  sofld  5500  cnvcnv  5505  dfco2  5551  unixp  5585  ressn  5588  fliftcnv  6461  fliftfun  6462  oprssdm  6713  frxp  7174  opeliunxp2f  7223  reltpos  7244  tpostpos  7259  tposfo  7266  tposf  7267  swoer  7659  xpider  7705  erinxp  7708  xpcomf1o  7934  cda1dif  8881  brdom3  9231  brdom5  9232  brdom4  9233  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  ordpinq  9644  addassnq  9659  mulassnq  9660  distrnq  9662  mulidnq  9664  recmulnq  9665  ltexnq  9676  prcdnq  9694  ltrel  9979  lerel  9981  dfle2  11856  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  0rest  15913  firest  15916  pwsle  15975  2oppchomf  16207  isinv  16243  invsym2  16246  invfun  16247  oppcsect2  16262  oppcinv  16263  oppchofcl  16723  oyoncl  16733  clatl  16939  gicer  17541  gicerOLD  17542  gsum2d2lem  18195  gsum2d2  18196  gsumcom2  18197  gsumxp  18198  dprd2d2  18266  opsrtoslem2  19306  mattpostpos  20079  mdetunilem9  20245  restbas  20772  txuni2  21178  txcls  21217  txdis1cn  21248  txkgen  21265  hmpher  21397  cnextrel  21677  tgphaus  21730  qustgplem  21734  tsmsxp  21768  utop2nei  21864  utop3cls  21865  xmeter  22048  caubl  22914  ovoliunlem1  23077  reldv  23440  taylf  23919  lgsquadlem1  24905  lgsquadlem2  24906  nvrel  26841  dfcnv2  28859  qtophaus  29231  cvmliftlem1  30521  cvmlift2lem12  30550  dfso2  30897  elrn3  30906  relbigcup  31174  poimirlem3  32582  heicant  32614  dvhopellsm  35424  dibvalrel  35470  dib1dim  35472  diclspsn  35501  dih1  35593  dih1dimatlem  35636  aoprssdm  39931  eliunxp2  41905
  Copyright terms: Public domain W3C validator