Theorem fnresi 6254

Description: Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.)

Assertion

Ref	Expression
fnresi	⊢ ( I ↾ 𝐴) Fn 𝐴

Proof of Theorem fnresi

Step	Hyp	Ref	Expression
1		funi 6167	. . 3 ⊢ Fun I
2		funres 6177	. . 3 ⊢ (Fun I → Fun ( I ↾ 𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ Fun ( I ↾ 𝐴)
4		dmresi 5713	. 2 ⊢ dom ( I ↾ 𝐴) = 𝐴
5		df-fn 6138	. 2 ⊢ (( I ↾ 𝐴) Fn 𝐴 ↔ (Fun ( I ↾ 𝐴) ∧ dom ( I ↾ 𝐴) = 𝐴))
6	3, 4, 5	mpbir2an 701	1 ⊢ ( I ↾ 𝐴) Fn 𝐴

Syntax hints:   = wceq 1601   I cid 5260  dom cdm 5355   ↾ cres 5357  Fun wfun 6129   Fn wfn 6130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-res 5367  df-fun 6137  df-fn 6138

This theorem is referenced by:  idssxpOLD  6255  f1oi  6428  fninfp  6707  fndifnfp  6709  fnnfpeq0  6711  fveqf1o  6829  weniso  6876  iordsmo  7737  fipreima  8560  dfac9  9293  pmtrfinv  18264  ustuqtop3  22455  fta1blem  24365  qaa  24515  dfiop2  29184  cvmliftlem4  31869  cvmliftlem5  31870  poimirlem15  34050  poimirlem22  34057  ltrnid  36289  rtrclex  38881  dvsid  39486  dflinc2  43214