Theorem fvmptelcdmf

Description: The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	fvmptelcdmf.a	⊢ Ⅎ 𝑥 𝐴
	fvmptelcdmf.c	⊢ Ⅎ 𝑥 𝐶
	fvmptelcdmf.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
Assertion	fvmptelcdmf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptelcdmf.a	⊢ Ⅎ 𝑥 𝐴
2		fvmptelcdmf.c	⊢ Ⅎ 𝑥 𝐶
3		fvmptelcdmf.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 2 4	fmptff	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
6	3 5	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
7	6	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )