Theorem fnresi 6635

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 6634	. 2 ⊢ I Fn V
2		ssv 3971	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6629	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 690	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:  Vcvv 3446   ⊆ wss 3913   I cid 5535   ↾ cres 5640   Fn wfn 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-res 5650  df-fun 6503  df-fn 6504

This theorem is referenced by:  f1oi  6827  fninfp  7125  fndifnfp  7127  fnnfpeq0  7129  fveqf1o  7254  weniso  7304  iordsmo  8308  fipreima  9309  dfac9  10081  smndex1n0mnd  18736  pmtrfinv  19257  ustuqtop3  23632  fta1blem  25570  qaa  25720  dfiop2  30758  symgcom2  32005  tocycfvres1  32029  tocycfvres2  32030  cvmliftlem4  33969  cvmliftlem5  33970  poimirlem15  36166  poimirlem22  36173  ltrnid  38671  dvsid  42733  dflinc2  46611