Theorem elrnmpt

Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015)

	Ref	Expression
Hypothesis	rnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	elrnmpt	$$⊢C\in V\to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2		eqeq1	$$⊢y=C\to \left(y=B\leftrightarrow C=B\right)$$
3	2	rexbidv	$$⊢y=C\to \left(\exists x\in Ay=B\leftrightarrow \exists x\in AC=B\right)$$
4	1	rnmpt	$$⊢\mathrm{ran}F=\left\{y|\exists x\in Ay=B\right\}$$
5	3 4	elab2g	$$⊢C\in V\to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$