Theorem ssrecnpr

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

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

Proof

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