Theorem resdm 6027

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906  dom cdm 5663   ↾ cres 5665  Rel wrel 5668

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-dm 5673  df-res 5675

This theorem is used by:  resindm  6031  resindmOLD  6032  reldmun  6035  reldisjunOLD  6036  relresdm1  6037  imadifssranOLD  6205  resdm2  6234  relresfldOLD  6281  fimadmfoALT  6807  fnex  7219  dftpos2  8241  tfrlem11  8377  tfrlem15  8381  tfrlem16  8382  pmresg  8870  domss2  9127  axdc3lem4  10448  gruima  10798  nosupbnd2lem1  27910  nosupbnd2  27911  noinfbnd2lem1  27925  noinfbnd2  27926  noetasuplem2  27929  noetasuplem3  27930  noetasuplem4  27931  noetainflem2  27933  bnj1321  35456  funsseq  36273  alrmomodm  39041  relbrcoss  39218  unidmqs  39421  releldmqs  39425  releldmqscoss  39427  seff  45052  sblpnf  45053  f1cof1blem  47844  funfocofob  47848  itcoval1  49476