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 𝐹 ∧ 𝐴 ∈ ( 𝐹 “ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ''' 𝑥 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elimag	⊢ ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) → ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 ) )
2	1	ibi	⊢ ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 )
3		funbrafv	⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝐴 → ( 𝐹 ''' 𝑥 ) = 𝐴 ) )
4	3	reximdv	⊢ ( Fun 𝐹 → ( ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ''' 𝑥 ) = 𝐴 ) )
5	2 4	syl5	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ''' 𝑥 ) = 𝐴 ) )
6	5	imp	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( 𝐹 “ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ''' 𝑥 ) = 𝐴 )