Theorem resdm 6010

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3924  dom cdm 5651   ↾ cres 5653  Rel wrel 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5117  df-opab 5179  df-xp 5657  df-rel 5658  df-dm 5661  df-res 5663

This theorem is referenced by:  resindm  6014  reldisjun  6016  relresdm1  6017  imadifssran  6137  resdm2  6217  relresfld  6262  fimadmfoALT  6797  fnex  7205  dftpos2  8236  tfrlem11  8396  tfrlem15  8400  tfrlem16  8401  pmresg  8878  domss2  9144  axdc3lem4  10459  gruima  10808  nosupbnd2lem1  27663  nosupbnd2  27664  noinfbnd2lem1  27678  noinfbnd2  27679  noetasuplem2  27682  noetasuplem3  27683  noetasuplem4  27684  noetainflem2  27686  bnj1321  34979  funsseq  35706  alrmomodm  38298  relbrcoss  38385  unidmqs  38593  releldmqs  38597  releldmqscoss  38599  seff  44259  sblpnf  44260  f1cof1blem  47031  funfocofob  47035  itcoval1  48529