Theorem recnprss

Description: Both RR and CC are subsets of CC . (Contributed by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Assertion	recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3		sseq1	$$⊢S=ℝ\to \left(S\subseteq ℂ\leftrightarrow ℝ\subseteq ℂ\right)$$
4	2 3	mpbiri	$$⊢S=ℝ\to S\subseteq ℂ$$
5		eqimss	$$⊢S=ℂ\to S\subseteq ℂ$$
6	4 5	jaoi	$$⊢\left(S=ℝ\vee S=ℂ\right)\to S\subseteq ℂ$$
7	1 6	syl	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$