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

Metamath Proof Explorer

Theorem fvrnressn

Description: If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018)

Ref Expression
Assertion fvrnressn ⊢ X ∈ V → F ⁡ X ∈ ran ⁡ F ↾ X → F ⁡ X ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 df-ima ⊢ F X = ran ⁡ F ↾ X
2 1 eleq2i ⊢ F ⁡ X ∈ F X ↔ F ⁡ X ∈ ran ⁡ F ↾ X
3 opeq1 ⊢ x = X → x F ⁡ X = X F ⁡ X
4 3 eleq1d ⊢ x = X → x F ⁡ X ∈ F ↔ X F ⁡ X ∈ F
5 4 spcegv ⊢ X ∈ V → X F ⁡ X ∈ F → ∃ x x F ⁡ X ∈ F
6 fvex ⊢ F ⁡ X ∈ V
7 elimasng ⊢ X ∈ V ∧ F ⁡ X ∈ V → F ⁡ X ∈ F X ↔ X F ⁡ X ∈ F
8 6 7 mpan2 ⊢ X ∈ V → F ⁡ X ∈ F X ↔ X F ⁡ X ∈ F
9 elrn2g ⊢ F ⁡ X ∈ V → F ⁡ X ∈ ran ⁡ F ↔ ∃ x x F ⁡ X ∈ F
10 6 9 mp1i ⊢ X ∈ V → F ⁡ X ∈ ran ⁡ F ↔ ∃ x x F ⁡ X ∈ F
11 5 8 10 3imtr4d ⊢ X ∈ V → F ⁡ X ∈ F X → F ⁡ X ∈ ran ⁡ F
12 2 11 biimtrrid ⊢ X ∈ V → F ⁡ X ∈ ran ⁡ F ↾ X → F ⁡ X ∈ ran ⁡ F