Theorem recnprss

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

	Ref	Expression
Assertion	recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		elpri	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
2		ax-resscn	⊢ ℝ ⊆ ℂ
3		sseq1	⊢ ( 𝑆 = ℝ → ( 𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ ) )
4	2 3	mpbiri	⊢ ( 𝑆 = ℝ → 𝑆 ⊆ ℂ )
5		eqimss	⊢ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ )
6	4 5	jaoi	⊢ ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝑆 ⊆ ℂ )
7	1 6	syl	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )