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

Theorem relres 4971
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 4681 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3365 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3183 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4782 . 2  |-  Rel  ( B  X.  _V )
5 relss 4763 . 2  |-  ( ( A  |`  B )  C_  ( B  X.  _V )  ->  ( Rel  ( B  X.  _V )  ->  Rel  ( A  |`  B ) ) )
63, 4, 5mp2 19 1  |-  Rel  ( A  |`  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2763    i^i cin 3126    C_ wss 3127    X. cxp 4659    |` cres 4663   Rel wrel 4666
This theorem is referenced by:  elres  4978  resiexg  4985  iss  4986  dfres2  4990  issref  5044  asymref  5047  poirr2  5055  cnvcnvres  5123  resco  5164  ressn  5198  funssres  5232  fnresdisj  5292  fnres  5298  fresaunres2  5351  fcnvres  5356  nfunsn  5492  dffv2  5526  fsnunfv  5654  resfunexgALT  5672  domss2  6988  fidomdm  7106  setsres  13137  pospo  14070  ovoliunlem1  18824  dvres  19224  dvres2  19225  dvlog  19961  efopnlem2  19967  h2hlm  21521  hlimcaui  21777  dfpo2  23484  dfrdg2  23522  funpartfun  23857  restidsing  24443  dispos  24655  mapfzcons1  26162  coeq0  26199  diophrw  26206  eldioph2lem1  26207  eldioph2lem2  26208
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-opab 4052  df-xp 4675  df-rel 4676  df-res 4681
  Copyright terms: Public domain W3C validator