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

Theorem relxp 5160
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 5159 . 2 (𝐴 × 𝐵) ⊆ (V × V)
2 df-rel 5150 . 2 (Rel (𝐴 × 𝐵) ↔ (𝐴 × 𝐵) ⊆ (V × V))
31, 2mpbir 221 1 Rel (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3231  wss 3607   × cxp 5141  Rel wrel 5148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149  df-rel 5150
This theorem is referenced by:  xpsspw  5266  xpiindi  5290  eliunxp  5292  opeliunxp2  5293  relres  5461  restidsing  5493  restidsingOLD  5494  codir  5551  qfto  5552  difxp  5593  sofld  5616  cnvcnv  5621  cnvcnvOLD  5622  dfco2  5672  unixp  5706  ressn  5709  fliftcnv  6601  fliftfun  6602  oprssdm  6857  frxp  7332  opeliunxp2f  7381  reltpos  7402  tpostpos  7417  tposfo  7424  tposf  7425  swoer  7817  xpider  7861  erinxp  7864  xpcomf1o  8090  cda1dif  9036  brdom3  9388  brdom5  9389  brdom4  9390  fpwwe2lem8  9497  fpwwe2lem9  9498  fpwwe2lem12  9501  ordpinq  9803  addassnq  9818  mulassnq  9819  distrnq  9821  mulidnq  9823  recmulnq  9824  ltexnq  9835  prcdnq  9853  ltrel  10138  lerel  10140  dfle2  12018  fsumcom2  14549  fsumcom2OLD  14550  fprodcom2  14758  fprodcom2OLD  14759  0rest  16137  firest  16140  pwsle  16199  2oppchomf  16431  isinv  16467  invsym2  16470  invfun  16471  oppcsect2  16486  oppcinv  16487  oppchofcl  16947  oyoncl  16957  clatl  17163  gicer  17765  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  gsumxp  18421  dprd2d2  18489  opsrtoslem2  19533  mattpostpos  20308  mdetunilem9  20474  restbas  21010  txuni2  21416  txcls  21455  txdis1cn  21486  txkgen  21503  hmpher  21635  cnextrel  21914  tgphaus  21967  qustgplem  21971  tsmsxp  22005  utop2nei  22101  utop3cls  22102  xmeter  22285  caubl  23152  ovoliunlem1  23316  reldv  23679  taylf  24160  lgsquadlem1  25150  lgsquadlem2  25151  nvrel  27585  dfcnv2  29604  qtophaus  30031  cvmliftlem1  31393  cvmlift2lem12  31422  dfso2  31770  elrn3  31778  relbigcup  32129  poimirlem3  33542  heicant  33574  vvdifopab  34165  inxprnres  34201  relinxp  34210  dvhopellsm  36723  dibvalrel  36769  dib1dim  36771  diclspsn  36800  dih1  36892  dih1dimatlem  36935  aoprssdm  41603  eliunxp2  42437
  Copyright terms: Public domain W3C validator