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

Theorem relres 4999
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  |-  Rel  ( A  |`  B )

Proof of Theorem relres
StepHypRef Expression
1 df-res 4717 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3403 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3221 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4810 . 2  |-  Rel  ( B  X.  _V )
5 relss 4791 . 2  |-  ( ( A  |`  B )  C_  ( B  X.  _V )  ->  ( Rel  ( B  X.  _V )  ->  Rel  ( A  |`  B ) ) )
63, 4, 5mp2 17 1  |-  Rel  ( A  |`  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2801    i^i cin 3164    C_ wss 3165    X. cxp 4703    |` cres 4707   Rel wrel 4710
This theorem is referenced by:  elres  5006  resiexg  5013  iss  5014  dfres2  5018  issref  5072  asymref  5075  poirr2  5083  cnvcnvres  5152  resco  5193  ressn  5227  funssres  5310  fnresdisj  5370  fnres  5376  fresaunres2  5429  fcnvres  5434  nfunsn  5574  dffv2  5608  fsnunfv  5736  resfunexgALT  5754  domss2  7036  fidomdm  7154  setsres  13190  pospo  14123  ovoliunlem1  18877  dvres  19277  dvres2  19278  dvlog  20014  efopnlem2  20020  h2hlm  21576  hlimcaui  21832  dmct  23357  dfpo2  24183  dfrdg2  24223  funpartfun  24553  restidsing  25179  dispos  25390  mapfzcons1  26897  coeq0  26934  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  funressnfv  28096  dfdfat2  28099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-opab 4094  df-xp 4711  df-rel 4712  df-res 4717
  Copyright terms: Public domain W3C validator