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

Metamath Proof Explorer

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 ⊢ Ⅎ _ x A
fvmptelcdmf.c ⊢ Ⅎ _ x C
fvmptelcdmf.f ⊢ φ → x ∈ A ⟼ B : A ⟶ C
Assertion fvmptelcdmf ⊢ φ ∧ x ∈ A → B ∈ C

Proof

Step Hyp Ref Expression
1 fvmptelcdmf.a ⊢ Ⅎ _ x A
2 fvmptelcdmf.c ⊢ Ⅎ _ x C
3 fvmptelcdmf.f ⊢ φ → x ∈ A ⟼ B : A ⟶ C
4 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
5 1 2 4 fmptff ⊢ ∀ x ∈ A B ∈ C ↔ x ∈ A ⟼ B : A ⟶ C
6 3 5 sylibr ⊢ φ → ∀ x ∈ A B ∈ C
7 6 r19.21bi ⊢ φ ∧ x ∈ A → B ∈ C