Theorem resdm 6000

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917  dom cdm 5641   ↾ cres 5643  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-dm 5651  df-res 5653

This theorem is referenced by:  resindm  6004  reldisjun  6006  relresdm1  6007  imadifssran  6127  resdm2  6207  relresfld  6252  fimadmfoALT  6786  fnex  7194  dftpos2  8225  tfrlem11  8359  tfrlem15  8363  tfrlem16  8364  pmresg  8846  domss2  9106  axdc3lem4  10413  gruima  10762  nosupbnd2lem1  27634  nosupbnd2  27635  noinfbnd2lem1  27649  noinfbnd2  27650  noetasuplem2  27653  noetasuplem3  27654  noetasuplem4  27655  noetainflem2  27657  bnj1321  35024  funsseq  35762  alrmomodm  38348  relbrcoss  38444  unidmqs  38653  releldmqs  38657  releldmqscoss  38659  seff  44305  sblpnf  44306  f1cof1blem  47079  funfocofob  47083  itcoval1  48656