Theorem resdm 5931

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888  dom cdm 5586   ↾ cres 5588  Rel wrel 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-br 5076  df-opab 5138  df-xp 5592  df-rel 5593  df-dm 5596  df-res 5598

This theorem is referenced by:  resindm  5935  resdm2  6129  relresfld  6174  fimadmfoALT  6693  fnex  7087  dftpos2  8048  tfrlem11  8208  tfrlem15  8212  tfrlem16  8213  pmresg  8647  domss2  8912  axdc3lem4  10198  gruima  10547  reldisjun  30929  funresdm1  30931  bnj1321  32994  funsseq  33729  nosupbnd2lem1  33905  nosupbnd2  33906  noinfbnd2lem1  33920  noinfbnd2  33921  noetasuplem2  33924  noetasuplem3  33925  noetasuplem4  33926  noetainflem2  33928  alrmomodm  36478  relbrcoss  36551  unidmqs  36753  releldmqs  36757  releldmqscoss  36759  seff  41887  sblpnf  41888  f1cof1blem  44525  funfocofob  44527  itcoval1  45966