MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reelprrecn Structured version   Unicode version

Theorem reelprrecn 9366
Description: Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
reelprrecn  |-  RR  e.  { RR ,  CC }

Proof of Theorem reelprrecn
StepHypRef Expression
1 reex 9365 . 2  |-  RR  e.  _V
21prid1 3978 1  |-  RR  e.  { RR ,  CC }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   {cpr 3874   CCcc 9272   RRcr 9273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-cnex 9330  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-sn 3873  df-pr 3875
This theorem is referenced by:  dvf  21357  dvmptcj  21417  dvmptre  21418  dvmptim  21419  rolle  21437  cmvth  21438  mvth  21439  dvlip  21440  dvlipcn  21441  dvle  21454  dvivthlem1  21455  dvivth  21457  lhop2  21462  dvcnvre  21466  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem2  21474  dvfsum2  21481  ftc2  21491  itgparts  21494  itgsubstlem  21495  aalioulem3  21775  taylthlem2  21814  taylth  21815  efcvx  21889  pige3  21954  dvrelog  22057  advlog  22074  advlogexp  22075  logccv  22083  dvcxp1  22155  loglesqr  22171  divsqrsumlem  22348  logexprlim  22539  logdivsum  22757  log2sumbnd  22768  lgamgulmlem2  26968  ftc2nc  28429  dvreasin  28435  dvreacos  28436  areacirclem1  28437  itgpowd  29543  lhe4.4ex1a  29556  dvcosre  29741  itgsin0pilem1  29743  itgsinexplem1  29747
  Copyright terms: Public domain W3C validator