# Metamath Proof Explorer

## Theorem elrnrexdm

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, 8-Dec-2017)

Ref Expression
Assertion elrnrexdm $⊢ Fun ⁡ F → Y ∈ ran ⁡ F → ∃ x ∈ dom ⁡ F Y = F ⁡ x$

### Proof

Step Hyp Ref Expression
1 eqidd $⊢ Y ∈ ran ⁡ F → Y = Y$
2 1 ancli $⊢ Y ∈ ran ⁡ F → Y ∈ ran ⁡ F ∧ Y = Y$
3 2 adantl $⊢ Fun ⁡ F ∧ Y ∈ ran ⁡ F → Y ∈ ran ⁡ F ∧ Y = Y$
4 eqeq2 $⊢ y = Y → Y = y ↔ Y = Y$
5 4 rspcev $⊢ Y ∈ ran ⁡ F ∧ Y = Y → ∃ y ∈ ran ⁡ F Y = y$
6 3 5 syl $⊢ Fun ⁡ F ∧ Y ∈ ran ⁡ F → ∃ y ∈ ran ⁡ F Y = y$
7 6 ex $⊢ Fun ⁡ F → Y ∈ ran ⁡ F → ∃ y ∈ ran ⁡ F Y = y$
8 funfn $⊢ Fun ⁡ F ↔ F Fn dom ⁡ F$
9 eqeq2 $⊢ y = F ⁡ x → Y = y ↔ Y = F ⁡ x$
10 9 rexrn $⊢ F Fn dom ⁡ F → ∃ y ∈ ran ⁡ F Y = y ↔ ∃ x ∈ dom ⁡ F Y = F ⁡ x$
11 8 10 sylbi $⊢ Fun ⁡ F → ∃ y ∈ ran ⁡ F Y = y ↔ ∃ x ∈ dom ⁡ F Y = F ⁡ x$
12 7 11 sylibd $⊢ Fun ⁡ F → Y ∈ ran ⁡ F → ∃ x ∈ dom ⁡ F Y = F ⁡ x$