Theorem fnresi 6558

Description: The restricted identity relation is a function on the restricting class. (Contributed by NM, 27-Aug-2004.) (Proof shortened by BJ, 27-Dec-2023.)

Assertion

Ref	Expression
fnresi	⊢ ( I ↾ 𝐴) Fn 𝐴

Proof of Theorem fnresi

Step	Hyp	Ref	Expression
1		idfn 6557	. 2 ⊢ I Fn V
2		ssv 3950	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6552	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 689	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:  Vcvv 3431   ⊆ wss 3892   I cid 5488   ↾ cres 5591   Fn wfn 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-res 5601  df-fun 6433  df-fn 6434

This theorem is referenced by:  f1oi  6750  fninfp  7041  fndifnfp  7043  fnnfpeq0  7045  fveqf1o  7169  weniso  7219  iordsmo  8177  fipreima  9101  dfac9  9891  smndex1n0mnd  18547  pmtrfinv  19065  ustuqtop3  23391  fta1blem  25329  qaa  25479  dfiop2  30109  symgcom2  31347  tocycfvres1  31371  tocycfvres2  31372  cvmliftlem4  33244  cvmliftlem5  33245  poimirlem15  35786  poimirlem22  35793  ltrnid  38143  dvsid  41917  dflinc2  45718