This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )