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