This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recnprss

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

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

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