Theorem resdm 6046

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963  dom cdm 5689   ↾ cres 5691  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-dm 5699  df-res 5701

This theorem is referenced by:  resindm  6050  reldisjun  6052  relresdm1  6053  resdm2  6253  relresfld  6298  fimadmfoALT  6832  fnex  7237  dftpos2  8267  tfrlem11  8427  tfrlem15  8431  tfrlem16  8432  pmresg  8909  domss2  9175  axdc3lem4  10491  gruima  10840  nosupbnd2lem1  27775  nosupbnd2  27776  noinfbnd2lem1  27790  noinfbnd2  27791  noetasuplem2  27794  noetasuplem3  27795  noetasuplem4  27796  noetainflem2  27798  bnj1321  35020  funsseq  35749  alrmomodm  38341  relbrcoss  38428  unidmqs  38636  releldmqs  38640  releldmqscoss  38642  seff  44305  sblpnf  44306  f1cof1blem  47024  funfocofob  47028  itcoval1  48513