Theorem afvelrnb

Description: A member of a function's range is a value of the function, analogous to fvelrnb with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvelrnb	|- ( ( F Fn A /\ B e. V ) -> ( 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	adantr	|- ( ( F Fn A /\ B e. V ) -> ran F = { y | E. x e. A y = ( F ''' x ) } )
3	2	eleq2d	|- ( ( F Fn A /\ B e. V ) -> ( B e. ran F <-> B e. { y | E. x e. A y = ( F ''' x ) } ) )
4		eqeq1	|- ( y = B -> ( y = ( F ''' x ) <-> B = ( F ''' x ) ) )
5		eqcom	|- ( B = ( F ''' x ) <-> ( F ''' x ) = B )
6	4 5	bitrdi	|- ( y = B -> ( y = ( F ''' x ) <-> ( F ''' x ) = B ) )
7	6	rexbidv	|- ( y = B -> ( E. x e. A y = ( F ''' x ) <-> E. x e. A ( F ''' x ) = B ) )
8	7	elabg	|- ( B e. V -> ( B e. { y | E. x e. A y = ( F ''' x ) } <-> E. x e. A ( F ''' x ) = B ) )
9	8	adantl	|- ( ( F Fn A /\ B e. V ) -> ( B e. { y | E. x e. A y = ( F ''' x ) } <-> E. x e. A ( F ''' x ) = B ) )
10	3 9	bitrd	|- ( ( F Fn A /\ B e. V ) -> ( B e. ran F <-> E. x e. A ( F ''' x ) = B ) )