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

Theorem relxp 5115
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

Proof of Theorem relxp
StepHypRef Expression
1 xpss 5114 . 2
2 df-rel 5011 . 2
31, 2mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:   cvv 3109  C_wss 3475  X.cxp 5002  Relwrel 5009
This theorem is referenced by:  xpsspwOLD  5122  xpiindi  5143  eliunxp  5145  opeliunxp2  5146  relres  5306  restidsing  5335  codir  5392  qfto  5393  difxp  5436  sofld  5460  cnvcnv  5464  dfco2  5511  unixp  5545  ressn  5548  fliftcnv  6209  fliftfun  6210  oprssdm  6456  frxp  6910  reltpos  6979  tpostpos  6994  tposfo  7001  tposf  7002  swoer  7358  xpider  7401  erinxp  7404  xpcomf1o  7626  cda1dif  8577  brdom3  8927  brdom5  8928  brdom4  8929  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  ordpinq  9342  addassnq  9357  mulassnq  9358  distrnq  9360  mulidnq  9362  recmulnq  9363  ltexnq  9374  prcdnq  9392  ltrel  9670  lerel  9672  dfle2  11382  fsumcom2  13589  fprodcom2  13788  0rest  14827  firest  14830  pwsle  14889  2oppchomf  15119  isinv  15154  invsym2  15157  invfun  15158  oppcsect2  15169  oppcinv  15170  oppchofcl  15529  oyoncl  15539  clatl  15746  gicer  16324  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  gsumxp  17004  gsumxpOLD  17006  dprd2d2  17093  opsrtoslem2  18149  mattpostpos  18956  mdetunilem9  19122  restbas  19659  txuni2  20066  txcls  20105  txdis1cn  20136  txkgen  20153  hmpher  20285  cnextrel  20563  tgphaus  20615  qustgplem  20619  tsmsxp  20657  utop2nei  20753  utop3cls  20754  xmeter  20936  caubl  21746  ovoliunlem1  21913  reldv  22274  taylf  22756  lgsquadlem1  23629  lgsquadlem2  23630  nvrel  25495  dfcnv2  27517  qtophaus  27839  cvmliftlem1  28730  cvmlift2lem12  28759  dfso2  29183  elrn3  29192  relbigcup  29547  heicant  30049  aoprssdm  32287  eliunxp2  32923  dvhopellsm  36844  dibvalrel  36890  dib1dim  36892  diclspsn  36921  dih1  37013  dih1dimatlem  37056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-opab 4511  df-xp 5010  df-rel 5011
  Copyright terms: Public domain W3C validator