Theorem fnresi 6668

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

This proof depends on syntax axioms:  Vcvv 3457   ⊆ wss 3906   I cid 5557   ↾ cres 5665   Fn wfn 6535

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-res 5675  df-fun 6542  df-fn 6543

This theorem is used by:  f1oi  6863  f1oiOLD  6864  fninfp  7178  fndifnfp  7180  fnnfpeq0  7182  fveqf1o  7309  weniso  7363  iordsmo  8350  fipreima  9322  dfac9  10136  smndex1n0mnd  19011  pmtrfinv  19575  psdmplcl  22375  ustuqtop3  24451  fta1blem  26379  qaa  26535  dfiop2  32176  symgcom2  33468  tocycfvres1  33494  tocycfvres2  33495  cvmliftlem4  35817  cvmliftlem5  35818  poimirlem15  38343  poimirlem22  38350  ltrnid  40967  dvsid  45099  cjnpoly  47684  dflinc2  49247  tposideq  49723