Theorem elrnmptd

Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	elrnmptd.f	$$⊢F=\left(x\in A⟼B\right)$$
	elrnmptd.x	$$⊢\phi \to \exists x\in AC=B$$
	elrnmptd.c	$$⊢\phi \to C\in V$$
Assertion	elrnmptd	$$⊢\phi \to C\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		elrnmptd.f	$$⊢F=\left(x\in A⟼B\right)$$
2		elrnmptd.x	$$⊢\phi \to \exists x\in AC=B$$
3		elrnmptd.c	$$⊢\phi \to C\in V$$
4	1	elrnmpt	$$⊢C\in V\to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$
5	3 4	syl	$$⊢\phi \to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$
6	2 5	mpbird	$$⊢\phi \to C\in \mathrm{ran}F$$