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

Theorem relres 4982
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 4700 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3391 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3209 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4793 . 2  |-  Rel  ( B  X.  _V )
5 relss 4774 . 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 2789    i^i cin 3152    C_ wss 3153    X. cxp 4686    |` cres 4690   Rel wrel 4693
This theorem is referenced by:  elres  4989  resiexg  4996  iss  4997  dfres2  5001  issref  5055  asymref  5058  poirr2  5066  cnvcnvres  5134  resco  5175  ressn  5209  funssres  5260  fnresdisj  5320  fnres  5326  fresaunres2  5379  fcnvres  5384  nfunsn  5520  dffv2  5554  fsnunfv  5682  resfunexgALT  5700  domss2  7016  fidomdm  7134  setsres  13170  pospo  14103  ovoliunlem1  18857  dvres  19257  dvres2  19258  dvlog  19994  efopnlem2  20000  h2hlm  21556  hlimcaui  21812  dfpo2  23518  dfrdg2  23556  funpartfun  23891  restidsing  24486  dispos  24698  mapfzcons1  26205  coeq0  26242  diophrw  26249  eldioph2lem1  26250  eldioph2lem2  26251  funressnfv  27382  dfdfat2  27385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-opab 4079  df-xp 4694  df-rel 4695  df-res 4700
  Copyright terms: Public domain W3C validator