Theorem fnresi 6476

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

Syntax hints:  Vcvv 3494   ⊆ wss 3936   I cid 5459   ↾ cres 5557   Fn wfn 6350

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-res 5567  df-fun 6357  df-fn 6358

This theorem is referenced by:  f1oi  6652  fninfp  6936  fndifnfp  6938  fnnfpeq0  6940  fveqf1o  7058  weniso  7107  iordsmo  7994  fipreima  8830  dfac9  9562  smndex1n0mnd  18077  pmtrfinv  18589  ustuqtop3  22852  fta1blem  24762  qaa  24912  dfiop2  29530  symgcom2  30728  tocycfvres1  30752  tocycfvres2  30753  cvmliftlem4  32535  cvmliftlem5  32536  poimirlem15  34922  poimirlem22  34929  ltrnid  37286  dvsid  40683  dflinc2  44485