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  18821  pmtrfinv  19375  psdmplcl  22082  ustuqtop3  24164  fta1blem  26109  qaa  26264  dfiop2  31732  symgcom2  33056  tocycfvres1  33082  tocycfvres2  33083  cvmliftlem4  35268  cvmliftlem5  35269  poimirlem15  37622  poimirlem22  37629  ltrnid  40122  dvsid  44313  cjnpoly  46883  dflinc2  48392  tposideq  48869