Theorem ssrecnpr

Description: RR is a subset of both RR and CC . (Contributed by Steve Rodriguez, 22-Nov-2015)

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

Proof

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