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

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

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