Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

	Ref	Expression
Assertion	fvelrnb	|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
2	1	eleq2d	|- ( F Fn A -> ( B e. ran F <-> B e. { y | E. x e. A y = ( F ` x ) } ) )
3		fvex	|- ( F ` x ) e. _V
4		eleq1	|- ( ( F ` x ) = B -> ( ( F ` x ) e. _V <-> B e. _V ) )
5	3 4	mpbii	|- ( ( F ` x ) = B -> B e. _V )
6	5	rexlimivw	|- ( E. x e. A ( F ` x ) = B -> B e. _V )
7		eqeq1	|- ( y = B -> ( y = ( F ` x ) <-> B = ( F ` x ) ) )
8		eqcom	|- ( B = ( F ` x ) <-> ( F ` x ) = B )
9	7 8	bitrdi	|- ( y = B -> ( y = ( F ` x ) <-> ( F ` x ) = B ) )
10	9	rexbidv	|- ( y = B -> ( E. x e. A y = ( F ` x ) <-> E. x e. A ( F ` x ) = B ) )
11	6 10	elab3	|- ( B e. { y | E. x e. A y = ( F ` x ) } <-> E. x e. A ( F ` x ) = B )
12	2 11	bitrdi	|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )