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

Theorem resdm 5890
Description: A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
Assertion
Ref Expression
resdm (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)

Proof of Theorem resdm
StepHypRef Expression
1 ssid 3986 . 2 dom 𝐴 ⊆ dom 𝐴
2 relssres 5886 . 2 ((Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → (𝐴 ↾ dom 𝐴) = 𝐴)
31, 2mpan2 687 1 (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3933  dom cdm 5548  cres 5550  Rel wrel 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-dm 5558  df-res 5560
This theorem is referenced by:  resindm  5893  resdm2  6081  relresfld  6120  fimadmfoALT  6594  fnex  6971  dftpos2  7898  tfrlem11  8013  tfrlem15  8017  tfrlem16  8018  pmresg  8423  domss2  8664  axdc3lem4  9863  gruima  10212  reldisjun  30281  funresdm1  30283  bnj1321  32196  funsseq  32908  nosupbnd2lem1  33112  nosupbnd2  33113  noetalem2  33115  noetalem3  33116  alrmomodm  35494  relbrcoss  35566  unidmqs  35768  releldmqs  35772  releldmqscoss  35774  seff  40518  sblpnf  40519
  Copyright terms: Public domain W3C validator