Theorem constcncfg

Description: A constant function is a continuous function on CC . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	constcncfg.a	$$⊢\phi \to A\subseteq ℂ$$
	constcncfg.b	$$⊢\phi \to B\in C$$
	constcncfg.c	$$⊢\phi \to C\subseteq ℂ$$
Assertion	constcncfg	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		constcncfg.a	$$⊢\phi \to A\subseteq ℂ$$
2		constcncfg.b	$$⊢\phi \to B\in C$$
3		constcncfg.c	$$⊢\phi \to C\subseteq ℂ$$
4		cncfmptc	$$⊢\left(B\in C\wedge A\subseteq ℂ\wedge C\subseteq ℂ\right)\to \left(x\in A⟼B\right):A\underset{cn}{⟶}C$$
5	2 1 3 4	syl3anc	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}C$$