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

Syntax hints:  Vcvv 3444   ⊆ wss 3911   I cid 5525   ↾ cres 5633   Fn wfn 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-fun 6501  df-fn 6502

This theorem is referenced by:  f1oi  6820  fninfp  7130  fndifnfp  7132  fnnfpeq0  7134  fveqf1o  7259  weniso  7311  iordsmo  8303  fipreima  9285  dfac9  10066  smndex1n0mnd  18815  pmtrfinv  19367  psdmplcl  22025  ustuqtop3  24107  fta1blem  26052  qaa  26207  dfiop2  31655  symgcom2  33014  tocycfvres1  33040  tocycfvres2  33041  cvmliftlem4  35248  cvmliftlem5  35249  poimirlem15  37602  poimirlem22  37609  ltrnid  40102  dvsid  44293  cjnpoly  46863  dflinc2  48372  tposideq  48849