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

Theorem relres 5414
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 (𝐴𝐵)

Proof of Theorem relres
StepHypRef Expression
1 df-res 5116 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss2 3826 . . 3 (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
31, 2eqsstri 3627 . 2 (𝐴𝐵) ⊆ (𝐵 × V)
4 relxp 5217 . 2 Rel (𝐵 × V)
5 relss 5196 . 2 ((𝐴𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴𝐵)))
63, 4, 5mp2 9 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3195  cin 3566  wss 3567   × cxp 5102  cres 5106  Rel wrel 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-opab 4704  df-xp 5110  df-rel 5111  df-res 5116
This theorem is referenced by:  elres  5423  iss  5435  dfres2  5441  restidsing  5446  restidsingOLD  5447  issref  5497  asymref  5500  poirr2  5508  cnvcnvres  5586  resco  5627  coeq0  5632  ressn  5659  funssres  5918  fnresdisj  5989  fnres  5995  fresaunres2  6063  fcnvres  6069  nfunsn  6212  dffv2  6258  fsnunfv  6438  resiexg  7087  resfunexgALT  7114  domss2  8104  fidomdm  8228  dmct  9331  relexp0rel  13758  setsres  15882  pospo  16954  metustid  22340  ovoliunlem1  23251  dvres  23656  dvres2  23657  dvlog  24378  efopnlem2  24384  h2hlm  27807  hlimcaui  28063  funresdm1  29388  dfpo2  31620  eqfunresadj  31635  dfrdg2  31675  funpartfun  32025  mapfzcons1  37099  diophrw  37141  eldioph2lem1  37142  eldioph2lem2  37143  undmrnresiss  37729  rtrclexi  37747  brfvrcld2  37803  relexpiidm  37815  rp-imass  37885  idhe  37901  limsupresuz  39735  liminfresuz  39810  funressnfv  40971  dfdfat2  40974  setrec2lem2  42206
  Copyright terms: Public domain W3C validator