Theorem afvelrnb0

Description: A member of a function's range is a value of the function, only one direction of implication of fvelrnb . (Contributed by Alexander van der Vekens, 1-Jun-2017)

	Ref	Expression
Assertion	afvelrnb0	|- ( F Fn A -> ( B e. ran F -> E. x e. A ( F ''' x ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnafv	|- ( 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		eqeq1	|- ( y = B -> ( y = ( F ''' x ) <-> B = ( F ''' x ) ) )
4		eqcom	|- ( B = ( F ''' x ) <-> ( F ''' x ) = B )
5	3 4	bitrdi	|- ( y = B -> ( y = ( F ''' x ) <-> ( F ''' x ) = B ) )
6	5	rexbidv	|- ( y = B -> ( E. x e. A y = ( F ''' x ) <-> E. x e. A ( F ''' x ) = B ) )
7	6	elabg	|- ( B e. { y | E. x e. A y = ( F ''' x ) } -> ( B e. { y | E. x e. A y = ( F ''' x ) } <-> E. x e. A ( F ''' x ) = B ) )
8	7	ibi	|- ( B e. { y | E. x e. A y = ( F ''' x ) } -> E. x e. A ( F ''' x ) = B )
9	2 8	biimtrdi	|- ( F Fn A -> ( B e. ran F -> E. x e. A ( F ''' x ) = B ) )