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

Theorem relres 5306
Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
relres

Proof of Theorem relres
StepHypRef Expression
1 df-res 5016 . . 3
2 inss2 3718 . . 3
31, 2eqsstri 3533 . 2
4 relxp 5115 . 2
5 relss 5095 . 2
63, 4, 5mp2 9 1
Colors of variables: wff setvar class
Syntax hints:   cvv 3109  i^icin 3474  C_wss 3475  X.cxp 5002  |`cres 5006  Relwrel 5009
This theorem is referenced by:  elres  5314  iss  5326  dfres2  5331  restidsing  5335  issref  5385  asymref  5388  poirr2  5396  cnvcnvres  5476  resco  5516  coeq0  5521  ressn  5548  funssres  5633  fnresdisj  5696  fnres  5702  fresaunres2  5762  fcnvres  5767  nfunsn  5902  dffv2  5946  fsnunfv  6111  resiexg  6736  resfunexgALT  6763  domss2  7696  fidomdm  7822  setsres  14660  pospo  15603  metustidOLD  21062  metustid  21063  ovoliunlem1  21913  dvres  22315  dvres2  22316  dvlog  23032  efopnlem2  23038  h2hlm  25897  hlimcaui  26154  dmct  27537  dfpo2  29184  dfrdg2  29228  funpartfun  29593  mapfzcons1  30649  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  funressnfv  32213  dfdfat2  32216  rp-imass  37795  idhe  37810
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  df-res 5016
  Copyright terms: Public domain W3C validator