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

Metamath Proof Explorer

Theorem axresscn

Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn . (Contributed by NM, 1-Mar-1995) (Proof shortened by Andrew Salmon, 12-Aug-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	axresscn	$⊢ ℝ \subseteq ℂ$

Proof

Step	Hyp	Ref	Expression
1		0r	$⊢ 0_{𝑹} \in 𝑹$
2		snssi	$⊢ 0_{𝑹} \in 𝑹 \to \{0_{𝑹}\} \subseteq 𝑹$
3		xpss2	$⊢ \{0_{𝑹}\} \subseteq 𝑹 \to 𝑹 \times \{0_{𝑹}\} \subseteq 𝑹 \times 𝑹$
4	1 2 3	mp2b	$⊢ 𝑹 \times \{0_{𝑹}\} \subseteq 𝑹 \times 𝑹$
5		df-r	$⊢ ℝ = 𝑹 \times \{0_{𝑹}\}$
6		df-c	$⊢ ℂ = 𝑹 \times 𝑹$
7	4 5 6	3sstr4i	$⊢ ℝ \subseteq ℂ$