Theorem elrnrexdmb

Description: For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017)

	Ref	Expression
Assertion	elrnrexdmb	⊢ ( Fun 𝐹 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2		fvelrnb	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑌 ) )
3	1 2	sylbi	⊢ ( Fun 𝐹 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑌 ) )
4		eqcom	⊢ ( 𝑌 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑌 )
5	4	rexbii	⊢ ( ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = 𝑌 )
6	3 5	bitr4di	⊢ ( Fun 𝐹 → ( 𝑌 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝑌 = ( 𝐹 ‘ 𝑥 ) ) )