Theorem afvelima

Description: Function value in an image, analogous to fvelima . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvelima	|- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ''' x ) = A )

Proof

Step	Hyp	Ref	Expression
1		elimag	|- ( A e. ( F " B ) -> ( A e. ( F " B ) <-> E. x e. B x F A ) )
2	1	ibi	|- ( A e. ( F " B ) -> E. x e. B x F A )
3		funbrafv	|- ( Fun F -> ( x F A -> ( F ''' x ) = A ) )
4	3	reximdv	|- ( Fun F -> ( E. x e. B x F A -> E. x e. B ( F ''' x ) = A ) )
5	2 4	syl5	|- ( Fun F -> ( A e. ( F " B ) -> E. x e. B ( F ''' x ) = A ) )
6	5	imp	|- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ''' x ) = A )