Theorem elrnmptf

Description: The range of a function in maps-to notation. Same as elrnmpt , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	elrnmptf.1	|- F/_ x C
	elrnmptf.2	|- F = ( x e. A |-> B )
Assertion	elrnmptf	|- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Proof

Step	Hyp	Ref	Expression
1		elrnmptf.1	|- F/_ x C
2		elrnmptf.2	|- F = ( x e. A |-> B )
3	1	nfeq2	|- F/ x y = C
4		eqeq1	|- ( y = C -> ( y = B <-> C = B ) )
5	3 4	rexbid	|- ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
6	2	rnmpt	|- ran F = { y | E. x e. A y = B }
7	5 6	elab2g	|- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )