Theorem resdm 5985

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

Syntax hints:   → wi 4   = wceq 1548   ⊆ wss 3885  dom cdm 5621   ↾ cres 5623  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-rel 5628  df-dm 5631  df-res 5633

This theorem is referenced by:  resindm  5989  reldisjun  5991  relresdm1  5992  imadifssran  6106  resdm2  6186  relresfld  6231  fimadmfoALT  6754  fnex  7165  dftpos2  8187  tfrlem11  8321  tfrlem15  8325  tfrlem16  8326  pmresg  8812  domss2  9068  axdc3lem4  10370  gruima  10720  nosupbnd2lem1  27701  nosupbnd2  27702  noinfbnd2lem1  27716  noinfbnd2  27717  noetasuplem2  27720  noetasuplem3  27721  noetasuplem4  27722  noetainflem2  27724  bnj1321  35224  funsseq  36011  alrmomodm  38741  relbrcoss  38918  unidmqs  39121  releldmqs  39125  releldmqscoss  39127  seff  44768  sblpnf  44769  f1cof1blem  47551  funfocofob  47555  itcoval1  49168