Theorem elrnmpt1d

Description: Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elrnmpt1d.1	$$⊢F=\left(x\in A⟼B\right)$$
	elrnmpt1d.2	$$⊢\phi \to x\in A$$
	elrnmpt1d.3	$$⊢\phi \to B\in V$$
Assertion	elrnmpt1d	$$⊢\phi \to B\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		elrnmpt1d.1	$$⊢F=\left(x\in A⟼B\right)$$
2		elrnmpt1d.2	$$⊢\phi \to x\in A$$
3		elrnmpt1d.3	$$⊢\phi \to B\in V$$
4	1	elrnmpt1	$$⊢\left(x\in A\wedge B\in V\right)\to B\in \mathrm{ran}F$$
5	2 3 4	syl2anc	$$⊢\phi \to B\in \mathrm{ran}F$$