Metamath Proof Explorer

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 ↾}_{A}) Fn A$

Proof

Step	Hyp	Ref	Expression
1		funi	$⊢ Fun I$
2		funres	$⊢ Fun I \to Fun ({I ↾}_{A})$
3	1 2	ax-mp	$⊢ Fun ({I ↾}_{A})$
4		dmresi	$⊢ dom ({I ↾}_{A}) = A$
5		df-fn	$⊢ ({I ↾}_{A}) Fn A \leftrightarrow (Fun ({I ↾}_{A}) \land dom ({I ↾}_{A}) = A)$
6	3 4 5	mpbir2an	$⊢ ({I ↾}_{A}) Fn A$