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	$$⊢F=\left(x\in A⟼B\right)$$
	rnmptc.a	$$⊢\phi \to A\ne \varnothing$$
Assertion	rnmptc	$$⊢\phi \to \mathrm{ran}F=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnmptc.f	$$⊢F=\left(x\in A⟼B\right)$$
2		rnmptc.a	$$⊢\phi \to A\ne \varnothing$$
3		fconstmpt	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
4	1 3	eqtr4i	$$⊢F=A\times \left\{B\right\}$$
5	4	rneqi	$$⊢\mathrm{ran}F=\mathrm{ran}\left(A\times \left\{B\right\}\right)$$
6		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times \left\{B\right\}\right)=\left\{B\right\}$$
7	5 6	syl5eq	$$⊢A\ne \varnothing \to \mathrm{ran}F=\left\{B\right\}$$
8	2 7	syl	$$⊢\phi \to \mathrm{ran}F=\left\{B\right\}$$