Theorem resdm 6013

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926  dom cdm 5654   ↾ cres 5656  Rel wrel 5659

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-dm 5664  df-res 5666

This theorem is referenced by:  resindm  6017  reldisjun  6019  relresdm1  6020  imadifssran  6140  resdm2  6220  relresfld  6265  fimadmfoALT  6801  fnex  7209  dftpos2  8242  tfrlem11  8402  tfrlem15  8406  tfrlem16  8407  pmresg  8884  domss2  9150  axdc3lem4  10467  gruima  10816  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem2  27702  bnj1321  35058  funsseq  35785  alrmomodm  38377  relbrcoss  38464  unidmqs  38672  releldmqs  38676  releldmqscoss  38678  seff  44333  sblpnf  44334  f1cof1blem  47103  funfocofob  47107  itcoval1  48643