Metamath Proof Explorer


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 𝐹 𝑌 = ( 𝐹𝑥 ) ) )