Theorem fnresiOLD

Description: Obsolete proof of fnresi as of 27-Dec-2023. (Contributed by NM, 27-Aug-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fnresiOLD	⊢ ( I ↾ 𝐴 ) Fn 𝐴

Proof

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