Theorem resdm 5997

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914  dom cdm 5638   ↾ cres 5640  Rel wrel 5643

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-dm 5648  df-res 5650

This theorem is referenced by:  resindm  6001  reldisjun  6003  relresdm1  6004  imadifssran  6124  resdm2  6204  relresfld  6249  fimadmfoALT  6783  fnex  7191  dftpos2  8222  tfrlem11  8356  tfrlem15  8360  tfrlem16  8361  pmresg  8843  domss2  9100  axdc3lem4  10406  gruima  10755  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd2lem1  27642  noinfbnd2  27643  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem2  27650  bnj1321  35017  funsseq  35755  alrmomodm  38341  relbrcoss  38437  unidmqs  38646  releldmqs  38650  releldmqscoss  38652  seff  44298  sblpnf  44299  f1cof1blem  47075  funfocofob  47079  itcoval1  48652