Theorem elrnmpt1sf

Description: Elementhood in an image set. Same as elrnmpt1s , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	elrnmpt1sf.1	|- F/_ x C
	elrnmpt1sf.2	|- F = ( x e. A |-> B )
	elrnmpt1sf.3	|- ( x = D -> B = C )
Assertion	elrnmpt1sf	|- ( ( D e. A /\ C e. V ) -> C e. ran F )

Proof

Step	Hyp	Ref	Expression
1		elrnmpt1sf.1	|- F/_ x C
2		elrnmpt1sf.2	|- F = ( x e. A |-> B )
3		elrnmpt1sf.3	|- ( x = D -> B = C )
4		eqid	|- C = C
5	1 1	nfeq	|- F/ x C = C
6	3	eqeq2d	|- ( x = D -> ( C = B <-> C = C ) )
7	5 6	rspce	|- ( ( D e. A /\ C = C ) -> E. x e. A C = B )
8	4 7	mpan2	|- ( D e. A -> E. x e. A C = B )
9	1 2	elrnmptf	|- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
10	9	biimparc	|- ( ( E. x e. A C = B /\ C e. V ) -> C e. ran F )
11	8 10	sylan	|- ( ( D e. A /\ C e. V ) -> C e. ran F )