ffvelcdm

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999)

		Ref	Expression
	Assertion	ffvelcdm	$⊢ (F : A ⟶ B \land C \in A) \to F (C) \in B$

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2		fnfvelrn	$⊢ (F Fn A \land C \in A) \to F (C) \in ran F$
3	1 2	sylan	$⊢ (F : A ⟶ B \land C \in A) \to F (C) \in ran F$
4		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
5	4	sseld	$⊢ F : A ⟶ B \to (F (C) \in ran F \to F (C) \in B)$
6	5	adantr	$⊢ (F : A ⟶ B \land C \in A) \to (F (C) \in ran F \to F (C) \in B)$
7	3 6	mpd	$⊢ (F : A ⟶ B \land C \in A) \to F (C) \in B$

Metamath Proof Explorer