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

Theorem relres 4983
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 4701 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3390 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3208 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4794 . 2  |-  Rel  ( B  X.  _V )
5 relss 4775 . 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 2788    i^i cin 3151    C_ wss 3152    X. cxp 4687    |` cres 4691   Rel wrel 4694
This theorem is referenced by:  elres  4990  resiexg  4997  iss  4998  dfres2  5002  issref  5056  asymref  5059  poirr2  5067  cnvcnvres  5136  resco  5177  ressn  5211  funssres  5294  fnresdisj  5354  fnres  5360  fresaunres2  5413  fcnvres  5418  nfunsn  5558  dffv2  5592  fsnunfv  5720  resfunexgALT  5738  domss2  7020  fidomdm  7138  setsres  13174  pospo  14107  ovoliunlem1  18861  dvres  19261  dvres2  19262  dvlog  19998  efopnlem2  20004  h2hlm  21560  hlimcaui  21816  dmct  23342  dfpo2  24112  dfrdg2  24152  funpartfun  24481  restidsing  25076  dispos  25287  mapfzcons1  26794  coeq0  26831  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  funressnfv  27991  dfdfat2  27994
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-opab 4078  df-xp 4695  df-rel 4696  df-res 4701
  Copyright terms: Public domain W3C validator