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

Metamath Proof Explorer

Theorem rnsnf

Description: The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses rnsnf.1 ⊢ φ → A ∈ V
rnsnf.2 ⊢ φ → F : A ⟶ B
Assertion rnsnf ⊢ φ → ran ⁡ F = F ⁡ A

Proof

Step Hyp Ref Expression
1 rnsnf.1 ⊢ φ → A ∈ V
2 rnsnf.2 ⊢ φ → F : A ⟶ B
3 elsni ⊢ x ∈ A → x = A
4 3 fveq2d ⊢ x ∈ A → F ⁡ x = F ⁡ A
5 4 mpteq2ia ⊢ x ∈ A ⟼ F ⁡ x = x ∈ A ⟼ F ⁡ A
6 2 feqmptd ⊢ φ → F = x ∈ A ⟼ F ⁡ x
7 fvexd ⊢ φ → F ⁡ A ∈ V
8 fmptsn ⊢ A ∈ V ∧ F ⁡ A ∈ V → A F ⁡ A = x ∈ A ⟼ F ⁡ A
9 1 7 8 syl2anc ⊢ φ → A F ⁡ A = x ∈ A ⟼ F ⁡ A
10 5 6 9 3eqtr4a ⊢ φ → F = A F ⁡ A
11 10 rneqd ⊢ φ → ran ⁡ F = ran ⁡ A F ⁡ A
12 rnsnopg ⊢ A ∈ V → ran ⁡ A F ⁡ A = F ⁡ A
13 1 12 syl ⊢ φ → ran ⁡ A F ⁡ A = F ⁡ A
14 11 13 eqtrd ⊢ φ → ran ⁡ F = F ⁡ A