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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fvbr0	⊢ ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ∨ ( 𝐹 ‘ 𝐴 ) = ∅ )
2		orcom	⊢ ( ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ∨ ( 𝐹 ‘ 𝐴 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝐴 ) = ∅ ∨ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
3	1 2	mpbi	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ ∨ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
4	3	ori	⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
5		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) ↔ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
6	5	rspcev	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
7	4 6	sylan2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
8		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
9	8	elima	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
10	7 9	sylibr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) )