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

Theorem relres 5086
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 4804 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3478 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3294 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4897 . 2  |-  Rel  ( B  X.  _V )
5 relss 4878 . 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 2873    i^i cin 3237    C_ wss 3238    X. cxp 4790    |` cres 4794   Rel wrel 4797
This theorem is referenced by:  elres  5093  resiexg  5100  iss  5101  dfres2  5105  issref  5159  asymref  5162  poirr2  5170  cnvcnvres  5239  resco  5280  ressn  5314  funssres  5397  fnresdisj  5459  fnres  5465  fresaunres2  5519  fcnvres  5524  nfunsn  5665  dffv2  5699  fsnunfv  5833  resfunexgALT  5858  domss2  7163  fidomdm  7285  setsres  13382  pospo  14317  ovoliunlem1  19076  dvres  19476  dvres2  19477  dvlog  20220  efopnlem2  20226  h2hlm  21873  hlimcaui  22129  dmct  23509  metustid  23797  dfpo2  24853  dfrdg2  24893  funpartfun  25223  mapfzcons1  26300  coeq0  26337  diophrw  26344  eldioph2lem1  26345  eldioph2lem2  26346  funressnfv  27499  dfdfat2  27502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-opab 4180  df-xp 4798  df-rel 4799  df-res 4804
  Copyright terms: Public domain W3C validator