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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	rnsnf.2	⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ 𝐵 )
Assertion	rnsnf	⊢ ( 𝜑 → ran 𝐹 = { ( 𝐹 ‘ 𝐴 ) } )

Proof

Step	Hyp	Ref	Expression
1		rnsnf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		rnsnf.2	⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ 𝐵 )
3		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
4	3	fveq2d	⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
5	4	mpteq2ia	⊢ ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) )
6	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝑥 ) ) )
7		fvexd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ V )
8		fmptsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) ) )
9	1 7 8	syl2anc	⊢ ( 𝜑 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ ( 𝐹 ‘ 𝐴 ) ) )
10	5 6 9	3eqtr4a	⊢ ( 𝜑 → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
11	10	rneqd	⊢ ( 𝜑 → ran 𝐹 = ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
12		rnsnopg	⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
13	1 12	syl	⊢ ( 𝜑 → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
14	11 13	eqtrd	⊢ ( 𝜑 → ran 𝐹 = { ( 𝐹 ‘ 𝐴 ) } )