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
|- RR e. { RR , CC }

Proof

Step Hyp Ref Expression
1 reex
 |-  RR e. _V
2 1 prid1
 |-  RR e. { RR , CC }