Theorem elrnmptg

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

	Ref	Expression
Hypothesis	rnmpt.1	|- F = ( x e. A |-> B )
Assertion	elrnmptg	|- ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	|- F = ( x e. A |-> B )
2	1	rnmpt	|- ran F = { y | E. x e. A y = B }
3	2	eleq2i	|- ( C e. ran F <-> C e. { y | E. x e. A y = B } )
4		r19.29	|- ( ( A. x e. A B e. V /\ E. x e. A C = B ) -> E. x e. A ( B e. V /\ C = B ) )
5		eleq1	|- ( C = B -> ( C e. V <-> B e. V ) )
6	5	biimparc	|- ( ( B e. V /\ C = B ) -> C e. V )
7	6	elexd	|- ( ( B e. V /\ C = B ) -> C e. _V )
8	7	rexlimivw	|- ( E. x e. A ( B e. V /\ C = B ) -> C e. _V )
9	4 8	syl	|- ( ( A. x e. A B e. V /\ E. x e. A C = B ) -> C e. _V )
10	9	ex	|- ( A. x e. A B e. V -> ( E. x e. A C = B -> C e. _V ) )
11		eqeq1	|- ( y = C -> ( y = B <-> C = B ) )
12	11	rexbidv	|- ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
13	12	elab3g	|- ( ( E. x e. A C = B -> C e. _V ) -> ( C e. { y | E. x e. A y = B } <-> E. x e. A C = B ) )
14	10 13	syl	|- ( A. x e. A B e. V -> ( C e. { y | E. x e. A y = B } <-> E. x e. A C = B ) )
15	3 14	bitrid	|- ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) )