Theorem resdm 6015

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

Step	Hyp	Ref	Expression
1		ssid 3953	. 2 ⊢ dom 𝐴 ⊆ dom 𝐴
2		relssres 6011	. 2 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → (𝐴 ↾ dom 𝐴) = 𝐴)
3	1, 2	mpan2 704	1 ⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899  dom cdm 5651   ↾ cres 5653  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-dm 5661  df-res 5663

This theorem is used by:  resindm  6019  resindmOLD  6020  reldmun  6023  reldisjunOLD  6024  relresdm1  6025  imadifssranOLDOLD  6202  resdm2  6231  relresfldOLD  6278  fimadmfoALT  6805  fnex  7221  dftpos2  8253  tfrlem11  8389  tfrlem15  8393  tfrlem16  8394  pmresg  8891  domss2  9148  axdc3lem4  10524  gruima  10880  nosupbnd2lem1  28065  nosupbnd2  28066  noinfbnd2lem1  28080  noinfbnd2  28081  noetasuplem2  28084  noetasuplem3  28085  noetasuplem4  28086  noetainflem2  28088  bnj1321  35650  funsseq  36512  alrmomodm  39271  relbrcoss  39448  unidmqs  39651  releldmqs  39655  releldmqscoss  39657  seff  45278  sblpnf  45279  f1cof1blem  48113  funfocofob  48117  itcoval1  49744