Theorem elrnmpt1s

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypotheses	rnmpt.1	|- F = ( x e. A |-> B )
	elrnmpt1s.1	|- ( x = D -> B = C )
Assertion	elrnmpt1s	|- ( ( D e. A /\ C e. V ) -> C e. ran F )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	|- F = ( x e. A |-> B )
2		elrnmpt1s.1	|- ( x = D -> B = C )
3		eqid	|- C = C
4	2	rspceeqv	|- ( ( D e. A /\ C = C ) -> E. x e. A C = B )
5	3 4	mpan2	|- ( D e. A -> E. x e. A C = B )
6	1	elrnmpt	|- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
7	6	biimparc	|- ( ( E. x e. A C = B /\ C e. V ) -> C e. ran F )
8	5 7	sylan	|- ( ( D e. A /\ C e. V ) -> C e. ran F )