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	$$⊢\underset{\_}{Ⅎ}xA$$
	fvmptelcdmf.c	$$⊢\underset{\_}{Ⅎ}xC$$
	fvmptelcdmf.f	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
Assertion	fvmptelcdmf	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptelcdmf.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		fvmptelcdmf.c	$$⊢\underset{\_}{Ⅎ}xC$$
3		fvmptelcdmf.f	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
4		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
5	1 2 4	fmptff	$$⊢\forall x\in AB\in C\leftrightarrow \left(x\in A⟼B\right):A⟶C$$
6	3 5	sylibr	$$⊢\phi \to \forall x\in AB\in C$$
7	6	r19.21bi	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$