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

Theorem relres 5114
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 4830 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3505 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3321 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4923 . 2  |-  Rel  ( B  X.  _V )
5 relss 4903 . 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 2899    i^i cin 3262    C_ wss 3263    X. cxp 4816    |` cres 4820   Rel wrel 4823
This theorem is referenced by:  elres  5121  resiexg  5128  iss  5129  dfres2  5133  issref  5187  asymref  5190  poirr2  5198  cnvcnvres  5273  resco  5314  ressn  5348  funssres  5433  fnresdisj  5495  fnres  5501  fresaunres2  5555  fcnvres  5560  nfunsn  5701  dffv2  5735  fsnunfv  5872  resfunexgALT  5897  domss2  7202  fidomdm  7324  setsres  13422  pospo  14357  metustid  18474  ovoliunlem1  19265  dvres  19665  dvres2  19666  dvlog  20409  efopnlem2  20415  h2hlm  22331  hlimcaui  22587  dmct  23947  dfpo2  25136  dfrdg2  25176  funpartfun  25506  mapfzcons1  26464  coeq0  26501  diophrw  26508  eldioph2lem1  26509  eldioph2lem2  26510  funressnfv  27661  dfdfat2  27664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-opab 4208  df-xp 4824  df-rel 4825  df-res 4830
  Copyright terms: Public domain W3C validator