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

Theorem relres 5166
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 4882 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3554 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3370 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4975 . 2  |-  Rel  ( B  X.  _V )
5 relss 4955 . 2  |-  ( ( A  |`  B )  C_  ( B  X.  _V )  ->  ( Rel  ( B  X.  _V )  ->  Rel  ( A  |`  B ) ) )
63, 4, 5mp2 9 1  |-  Rel  ( A  |`  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2948    i^i cin 3311    C_ wss 3312    X. cxp 4868    |` cres 4872   Rel wrel 4875
This theorem is referenced by:  elres  5173  resiexg  5180  iss  5181  dfres2  5185  issref  5239  asymref  5242  poirr2  5250  cnvcnvres  5325  resco  5366  ressn  5400  funssres  5485  fnresdisj  5547  fnres  5553  fresaunres2  5607  fcnvres  5612  nfunsn  5753  dffv2  5788  fsnunfv  5925  resfunexgALT  5950  domss2  7258  fidomdm  7380  setsres  13487  pospo  14422  metustidOLD  18581  metustid  18582  ovoliunlem1  19390  dvres  19790  dvres2  19791  dvlog  20534  efopnlem2  20540  h2hlm  22475  hlimcaui  22731  dmct  24098  dfpo2  25370  dfrdg2  25415  funpartfun  25780  mapfzcons1  26754  coeq0  26791  diophrw  26798  eldioph2lem1  26799  eldioph2lem2  26800  funressnfv  27949  dfdfat2  27952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-opab 4259  df-xp 4876  df-rel 4877  df-res 4882
  Copyright terms: Public domain W3C validator