fun2ssres

Description: Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994)

		Ref	Expression
	Assertion	fun2ssres	$⊢ (Fun F \land G \subseteq F \land A \subseteq dom G) \to {F ↾}_{A} = {G ↾}_{A}$

Step	Hyp	Ref	Expression
1		resabs1	$⊢ A \subseteq dom G \to {({F ↾}_{dom G}) ↾}_{A} = {F ↾}_{A}$
2	1	eqcomd	$⊢ A \subseteq dom G \to {F ↾}_{A} = {({F ↾}_{dom G}) ↾}_{A}$
3		funssres	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$
4	3	reseq1d	$⊢ (Fun F \land G \subseteq F) \to {({F ↾}_{dom G}) ↾}_{A} = {G ↾}_{A}$
5	2 4	sylan9eqr	$⊢ ((Fun F \land G \subseteq F) \land A \subseteq dom G) \to {F ↾}_{A} = {G ↾}_{A}$
6	5	3impa	$⊢ (Fun F \land G \subseteq F \land A \subseteq dom G) \to {F ↾}_{A} = {G ↾}_{A}$

Metamath Proof Explorer