Theorem constcncfg

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

	Ref	Expression
Hypotheses	constcncfg.a	|- ( ph -> A C_ CC )
	constcncfg.b	|- ( ph -> B e. C )
	constcncfg.c	|- ( ph -> C C_ CC )
Assertion	constcncfg	|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )

Proof

Step	Hyp	Ref	Expression
1		constcncfg.a	|- ( ph -> A C_ CC )
2		constcncfg.b	|- ( ph -> B e. C )
3		constcncfg.c	|- ( ph -> C C_ CC )
4		cncfmptc	|- ( ( B e. C /\ A C_ CC /\ C C_ CC ) -> ( x e. A |-> B ) e. ( A -cn-> C ) )
5	2 1 3 4	syl3anc	|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )