Theorem reelprrecn 9587

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

Syntax hints:   e. wcel 1804   {cpr 4016   CCcc 9493   RRcr 9494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-cnex 9551  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-sn 4015  df-pr 4017

This theorem is referenced by:  dvf  22288  dvmptcj  22348  dvmptre  22349  dvmptim  22350  rolle  22368  cmvth  22369  mvth  22370  dvlip  22371  dvlipcn  22372  dvle  22385  dvivthlem1  22386  dvivth  22388  lhop2  22393  dvcnvre  22397  dvfsumle  22399  dvfsumge  22400  dvfsumabs  22401  dvfsumlem2  22405  dvfsum2  22412  ftc2  22422  itgparts  22425  itgsubstlem  22426  aalioulem3  22706  taylthlem2  22745  taylth  22746  efcvx  22820  pige3  22886  dvrelog  22994  advlog  23011  advlogexp  23012  logccv  23020  dvcxp1  23092  loglesqrt  23108  divsqrtsumlem  23285  logexprlim  23476  logdivsum  23694  log2sumbnd  23705  lgamgulmlem2  28549  ftc2nc  30074  dvreasin  30080  dvreacos  30081  areacirclem1  30082  itgpowd  31158  lhe4.4ex1a  31210  dvcosre  31610  dvcnre  31615  dvmptresicc  31620  itgsin0pilem1  31638  itgsinexplem1  31642  itgcoscmulx  31658  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  dirkeritg  31773  dirkercncflem2  31775  fourierdlem28  31806  fourierdlem39  31817  fourierdlem56  31834  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem60  31838  fourierdlem61  31839  fourierdlem62  31840  fourierdlem68  31846  fourierdlem72  31850  fouriersw  31903