Theorem eliman0

Description: A nonempty function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019)

	Ref	Expression
Assertion	eliman0	|- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( F " B ) )

Proof

Step	Hyp	Ref	Expression
1		fvbr0	|- ( A F ( F ` A ) \/ ( F ` A ) = (/) )
2		orcom	|- ( ( A F ( F ` A ) \/ ( F ` A ) = (/) ) <-> ( ( F ` A ) = (/) \/ A F ( F ` A ) ) )
3	1 2	mpbi	|- ( ( F ` A ) = (/) \/ A F ( F ` A ) )
4	3	ori	|- ( -. ( F ` A ) = (/) -> A F ( F ` A ) )
5		breq1	|- ( x = A -> ( x F ( F ` A ) <-> A F ( F ` A ) ) )
6	5	rspcev	|- ( ( A e. B /\ A F ( F ` A ) ) -> E. x e. B x F ( F ` A ) )
7	4 6	sylan2	|- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> E. x e. B x F ( F ` A ) )
8		fvex	|- ( F ` A ) e. _V
9	8	elima	|- ( ( F ` A ) e. ( F " B ) <-> E. x e. B x F ( F ` A ) )
10	7 9	sylibr	|- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( F " B ) )