Theorem resdm 6025

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905  dom cdm 5661   ↾ cres 5663  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-dm 5671  df-res 5673

This theorem is referenced by:  resindm  6029  resindmOLD  6030  reldmun  6033  reldisjunOLD  6034  relresdm1  6035  imadifssranOLD  6203  resdm2  6232  relresfld  6277  fimadmfoALT  6803  fnex  7215  dftpos2  8235  tfrlem11  8371  tfrlem15  8375  tfrlem16  8376  pmresg  8864  domss2  9120  axdc3lem4  10432  gruima  10782  nosupbnd2lem1  27879  nosupbnd2  27880  noinfbnd2lem1  27894  noinfbnd2  27895  noetasuplem2  27898  noetasuplem3  27899  noetasuplem4  27900  noetainflem2  27902  bnj1321  35415  funsseq  36260  alrmomodm  39008  relbrcoss  39185  unidmqs  39388  releldmqs  39392  releldmqscoss  39394  seff  45019  sblpnf  45020  f1cof1blem  47811  funfocofob  47815  itcoval1  49443