Theorem elrnmpti

Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2		elrnmpti.2	$$⊢B\in \mathrm{V}$$
3	2	rgenw	$$⊢\forall x\in AB\in \mathrm{V}$$
4	1	elrnmptg	$$⊢\forall x\in AB\in \mathrm{V}\to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$
5	3 4	ax-mp	$$⊢C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B$$