Theorem fnresi 6629

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 6628	. 2 ⊢ I Fn V
2		ssv 3960	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6623	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 693	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:  Vcvv 3442   ⊆ wss 3903   I cid 5526   ↾ cres 5634   Fn wfn 6495

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-res 5644  df-fun 6502  df-fn 6503

This theorem is referenced by:  f1oi  6820  f1oiOLD  6821  fninfp  7130  fndifnfp  7132  fnnfpeq0  7134  fveqf1o  7258  weniso  7310  iordsmo  8299  fipreima  9270  dfac9  10059  smndex1n0mnd  18849  pmtrfinv  19402  psdmplcl  22117  ustuqtop3  24199  fta1blem  26144  qaa  26299  dfiop2  31841  symgcom2  33178  tocycfvres1  33204  tocycfvres2  33205  cvmliftlem4  35504  cvmliftlem5  35505  poimirlem15  37886  poimirlem22  37893  ltrnid  40511  dvsid  44687  cjnpoly  47249  dflinc2  48770  tposideq  49247