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 ∈ B ∧ ¬ F ⁡ A = ∅ → F ⁡ A ∈ 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 ∈ B ∧ A F F ⁡ A → ∃ x ∈ B x F F ⁡ A
7 4 6 sylan2 ⊢ A ∈ B ∧ ¬ F ⁡ A = ∅ → ∃ x ∈ B x F F ⁡ A
8 fvex ⊢ F ⁡ A ∈ V
9 8 elima ⊢ F ⁡ A ∈ F B ↔ ∃ x ∈ B x F F ⁡ A
10 7 9 sylibr ⊢ A ∈ B ∧ ¬ F ⁡ A = ∅ → F ⁡ A ∈ F B