This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funssfv

Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994)

		Ref	Expression
	Assertion	funssfv	$⊢ (Fun F \land G \subseteq F \land A \in dom G) \to F (A) = G (A)$

Step	Hyp	Ref	Expression
1		fvres	$⊢ A \in dom G \to ({F ↾}_{dom G}) (A) = F (A)$
2	1	eqcomd	$⊢ A \in dom G \to F (A) = ({F ↾}_{dom G}) (A)$
3		funssres	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$
4	3	fveq1d	$⊢ (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 \in dom G) \to F (A) = G (A)$
6	5	3impa	$⊢ (Fun F \land G \subseteq F \land A \in dom G) \to F (A) = G (A)$