Theorem idcncfg

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

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

Proof

Step	Hyp	Ref	Expression
1		idcncfg.a	$$⊢\phi \to A\subseteq B$$
2		idcncfg.b	$$⊢\phi \to B\subseteq ℂ$$
3		cncfmptid	$$⊢\left(A\subseteq B\wedge B\subseteq ℂ\right)\to \left(x\in A⟼x\right):A\underset{cn}{⟶}B$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(x\in A⟼x\right):A\underset{cn}{⟶}B$$