Theorem fnresi 6614

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 6613	. 2 ⊢ I Fn V
2		ssv 3939	. 2 ⊢ 𝐴 ⊆ V
3		fnssres 6608	. 2 ⊢ (( I Fn V ∧ 𝐴 ⊆ V) → ( I ↾ 𝐴) Fn 𝐴)
4	1, 2, 3	mp2an 698	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:  Vcvv 3431   ⊆ wss 3883   I cid 5512   ↾ cres 5620   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-res 5630  df-fun 6487  df-fn 6488

This theorem is referenced by:  f1oi  6805  f1oiOLD  6806  fninfp  7118  fndifnfp  7120  fnnfpeq0  7122  fveqf1o  7246  weniso  7298  iordsmo  8287  fipreima  9258  dfac9  10050  smndex1n0mnd  18874  pmtrfinv  19427  psdmplcl  22150  ustuqtop3  24226  fta1blem  26154  qaa  26307  dfiop2  31842  symgcom2  33165  tocycfvres1  33191  tocycfvres2  33192  cvmliftlem4  35516  cvmliftlem5  35517  poimirlem15  38002  poimirlem22  38009  ltrnid  40627  dvsid  44775  cjnpoly  47352  dflinc2  48901  tposideq  49378