Theorem resdm 5899

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3938  dom cdm 5557   ↾ cres 5559  Rel wrel 5562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-dm 5567  df-res 5569

This theorem is referenced by:  resindm  5902  resdm2  6090  relresfld  6129  fimadmfoALT  6603  fnex  6982  dftpos2  7911  tfrlem11  8026  tfrlem15  8030  tfrlem16  8031  pmresg  8436  domss2  8678  axdc3lem4  9877  gruima  10226  reldisjun  30355  funresdm1  30357  bnj1321  32301  funsseq  33013  nosupbnd2lem1  33217  nosupbnd2  33218  noetalem2  33220  noetalem3  33221  alrmomodm  35615  relbrcoss  35688  unidmqs  35890  releldmqs  35894  releldmqscoss  35896  seff  40648  sblpnf  40649