Theorem eldmrexrn

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

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

Proof

Step	Hyp	Ref	Expression
1		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑌 ) ∈ ran 𝐹 )
2		eqid	⊢ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 )
3		eqeq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑌 ) → ( 𝑥 = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) ) )
4	3	rspcev	⊢ ( ( ( 𝐹 ‘ 𝑌 ) ∈ ran 𝐹 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) ) → ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹 ‘ 𝑌 ) )
5	1 2 4	sylancl	⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ dom 𝐹 ) → ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹 ‘ 𝑌 ) )
6	5	ex	⊢ ( Fun 𝐹 → ( 𝑌 ∈ dom 𝐹 → ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹 ‘ 𝑌 ) ) )