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 = ( x e. A |-> B )
	elrnmpti.2	|- B e. _V
Assertion	elrnmpti	|- ( C e. ran F <-> E. x e. A C = B )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	|- F = ( x e. A |-> B )
2		elrnmpti.2	|- B e. _V
3	2	rgenw	|- A. x e. A B e. _V
4	1	elrnmptg	|- ( A. x e. A B e. _V -> ( C e. ran F <-> E. x e. A C = B ) )
5	3 4	ax-mp	|- ( C e. ran F <-> E. x e. A C = B )