This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ F → Y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F Y = F ⁡ x

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 fvelrnb ⊢ F Fn dom ⁡ F → Y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F F ⁡ x = Y
3 1 2 sylbi ⊢ Fun ⁡ F → Y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F F ⁡ x = Y
4 eqcom ⊢ Y = F ⁡ x ↔ F ⁡ x = Y
5 4 rexbii ⊢ ∃ x ∈ dom ⁡ F Y = F ⁡ x ↔ ∃ x ∈ dom ⁡ F F ⁡ x = Y
6 3 5 bitr4di ⊢ Fun ⁡ F → Y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F Y = F ⁡ x