Theorem fnresi 6661

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 6660	. 2 ⊢ I Fn V
2		ssv 3955	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6655	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 705	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3899   I cid 5549   ↾ cres 5657   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-res 5667  df-fun 6535  df-fn 6536

This theorem is used by:  f1oi  6856  f1oiOLD  6857  fninfp  7172  fndifnfp  7174  fnnfpeq0  7176  fveqf1o  7303  weniso  7357  iordsmo  8346  fipreima  9325  dfac9  10139  smndex1n0mnd  19024  pmtrfinv  19588  psdmplcl  22390  ustuqtop3  24469  fta1blem  26396  qaa  26556  dfiop2  32234  symgcom2  33524  tocycfvres1  33550  tocycfvres2  33551  cvmliftlem4  35867  cvmliftlem5  35868  poimirlem15  38384  poimirlem22  38391  ltrnid  41008  dvsid  45155  cjnpoly  47757  dflinc2  49340  tposideq  49814