Theorem fnresi 6621

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 6620	. 2 ⊢ I Fn V
2		ssv 3958	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6615	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 692	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:  Vcvv 3440   ⊆ wss 3901   I cid 5518   ↾ cres 5626   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-res 5636  df-fun 6494  df-fn 6495

This theorem is referenced by:  f1oi  6812  f1oiOLD  6813  fninfp  7120  fndifnfp  7122  fnnfpeq0  7124  fveqf1o  7248  weniso  7300  iordsmo  8289  fipreima  9258  dfac9  10047  smndex1n0mnd  18837  pmtrfinv  19390  psdmplcl  22105  ustuqtop3  24187  fta1blem  26132  qaa  26287  dfiop2  31828  symgcom2  33166  tocycfvres1  33192  tocycfvres2  33193  cvmliftlem4  35482  cvmliftlem5  35483  poimirlem15  37836  poimirlem22  37843  ltrnid  40395  dvsid  44572  cjnpoly  47135  dflinc2  48656  tposideq  49133