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

Theorem relres 4985
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 4703 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3392 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3210 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4796 . 2  |-  Rel  ( B  X.  _V )
5 relss 4777 . 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 2790    i^i cin 3153    C_ wss 3154    X. cxp 4689    |` cres 4693   Rel wrel 4696
This theorem is referenced by:  elres  4992  resiexg  4999  iss  5000  dfres2  5004  issref  5058  asymref  5061  poirr2  5069  cnvcnvres  5138  resco  5179  ressn  5213  funssres  5296  fnresdisj  5356  fnres  5362  fresaunres2  5415  fcnvres  5420  nfunsn  5560  dffv2  5594  fsnunfv  5722  resfunexgALT  5740  domss2  7022  fidomdm  7140  setsres  13176  pospo  14109  ovoliunlem1  18863  dvres  19263  dvres2  19264  dvlog  20000  efopnlem2  20006  h2hlm  21562  hlimcaui  21818  dmct  23344  dfpo2  24114  dfrdg2  24154  funpartfun  24483  restidsing  25087  dispos  25298  mapfzcons1  26805  coeq0  26842  diophrw  26849  eldioph2lem1  26850  eldioph2lem2  26851  funressnfv  28002  dfdfat2  28005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-opab 4080  df-xp 4697  df-rel 4698  df-res 4703
  Copyright terms: Public domain W3C validator