Theorem reelprrecn 9656

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 9655	. 2 |- RR e. _V
2	1	prid1 4092	1 |- RR e. { RR , CC }

Syntax hints:   e. wcel 1897   {cpr 3981   CCcc 9562   RRcr 9563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-cnex 9620  ax-resscn 9621

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429  df-sn 3980  df-pr 3982

This theorem is referenced by:  dvf  22910  dvmptcj  22970  dvmptre  22971  dvmptim  22972  rolle  22990  cmvth  22991  mvth  22992  dvlip  22993  dvlipcn  22994  dvle  23007  dvivthlem1  23008  dvivth  23010  lhop2  23015  dvcnvre  23019  dvfsumle  23021  dvfsumge  23022  dvfsumabs  23023  dvfsumlem2  23027  dvfsum2  23034  ftc2  23044  itgparts  23047  itgsubstlem  23048  aalioulem3  23338  taylthlem2  23377  taylth  23378  efcvx  23452  pige3  23520  dvrelog  23630  advlog  23647  advlogexp  23648  logccv  23656  dvcxp1  23728  loglesqrt  23746  divsqrtsumlem  23953  lgamgulmlem2  24003  logexprlim  24201  logdivsum  24419  log2sumbnd  24430  ftc2nc  32070  dvreasin  32074  dvreacos  32075  areacirclem1  32076  itgpowd  36143  lhe4.4ex1a  36721  dvcosre  37818  dvcnre  37823  dvmptresicc  37828  itgsin0pilem1  37863  itgsinexplem1  37867  itgcoscmulx  37883  itgiccshift  37894  itgperiod  37895  itgsbtaddcnst  37896  dirkeritg  38001  dirkercncflem2  38003  fourierdlem28  38034  fourierdlem39  38046  fourierdlem56  38063  fourierdlem57  38064  fourierdlem58  38065  fourierdlem59  38066  fourierdlem60  38067  fourierdlem61  38068  fourierdlem62  38069  fourierdlem68  38075  fourierdlem72  38079  fouriersw  38132  etransclem2  38138  etransclem23  38159  etransclem35  38171  etransclem38  38174  etransclem39  38175  etransclem44  38180  etransclem45  38181  etransclem46  38182  etransclem47  38183