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

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 }