Theorem fvmptelrn

Description: The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	fvmptelrn.1	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
Assertion	fvmptelrn	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptelrn.1	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
2		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
3	2	fmpt	$$⊢\forall x\in AB\in C\leftrightarrow \left(x\in A⟼B\right):A⟶C$$
4	1 3	sylibr	$$⊢\phi \to \forall x\in AB\in C$$
5	4	r19.21bi	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$