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

Theorem resdm 5736
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 3875 . 2 dom 𝐴 ⊆ dom 𝐴
2 relssres 5732 . 2 ((Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → (𝐴 ↾ dom 𝐴) = 𝐴)
31, 2mpan2 678 1 (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1507  wss 3825  dom cdm 5400  cres 5402  Rel wrel 5405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pr 5180
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-xp 5406  df-rel 5407  df-dm 5410  df-res 5412
This theorem is referenced by:  resindm  5739  resdm2  5921  relresfld  5959  fimadmfoALT  6424  fnex  6800  dftpos2  7705  tfrlem11  7821  tfrlem15  7825  tfrlem16  7826  pmresg  8226  domss2  8464  axdc3lem4  9665  gruima  10014  funresdm1  30109  bnj1321  31905  funsseq  32471  nosupbnd2lem1  32676  nosupbnd2  32677  noetalem2  32679  noetalem3  32680  alrmomodm  35007  relbrcoss  35079  unidmqs  35281  releldmqs  35285  releldmqscoss  35287  seff  40001  sblpnf  40002
  Copyright terms: Public domain W3C validator