Theorem rnmptc

Description: Range of a constant function in maps-to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019) Remove extra hypothesis. (Revised by SN, 17-Apr-2024)

	Ref	Expression
Hypotheses	rnmptc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rnmptc.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	rnmptc	⊢ ( 𝜑 → ran 𝐹 = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		rnmptc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		rnmptc.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	1 3	eqtr4i	⊢ 𝐹 = ( 𝐴 × { 𝐵 } )
5	4	rneqi	⊢ ran 𝐹 = ran ( 𝐴 × { 𝐵 } )
6		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × { 𝐵 } ) = { 𝐵 } )
7	5 6	syl5eq	⊢ ( 𝐴 ≠ ∅ → ran 𝐹 = { 𝐵 } )
8	2 7	syl	⊢ ( 𝜑 → ran 𝐹 = { 𝐵 } )