Metamath Proof Explorer


Theorem reelprrecn

Description: Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion reelprrecn ⊢ ℝ ∈ ℝ ℂ

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 1 prid1 ⊢ ℝ ∈ ℝ ℂ