Theorem resdm 5978

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 3937	. 2 ⊢ dom 𝐴 ⊆ dom 𝐴
2		relssres 5974	. 2 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴) → (𝐴 ↾ dom 𝐴) = 𝐴)
3	1, 2	mpan2 697	1 ⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883  dom cdm 5618   ↾ cres 5620  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-dm 5628  df-res 5630

This theorem is referenced by:  resindm  5982  reldisjun  5984  relresdm1  5985  imadifssran  6102  resdm2  6182  relresfld  6227  fimadmfoALT  6750  fnex  7161  dftpos2  8183  tfrlem11  8317  tfrlem15  8321  tfrlem16  8322  pmresg  8808  domss2  9064  axdc3lem4  10366  gruima  10716  nosupbnd2lem1  27697  nosupbnd2  27698  noinfbnd2lem1  27712  noinfbnd2  27713  noetasuplem2  27716  noetasuplem3  27717  noetasuplem4  27718  noetainflem2  27720  bnj1321  35209  funsseq  35996  alrmomodm  38726  relbrcoss  38903  unidmqs  39106  releldmqs  39110  releldmqscoss  39112  seff  44753  sblpnf  44754  f1cof1blem  47537  funfocofob  47541  itcoval1  49154