Theorem reelprrecn 11204

Description: Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
reelprrecn	⊢ ℝ ∈ {ℝ, ℂ}

Proof of Theorem reelprrecn

Step	Hyp	Ref	Expression
1		reex 11203	. 2 ⊢ ℝ ∈ V
2	1	prid1 4766	1 ⊢ ℝ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2106  {cpr 4630  ℂcc 11110  ℝcr 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631

This theorem is referenced by:  dvf  25431  dvmptresicc  25440  dvmptcj  25492  dvmptre  25493  dvmptim  25494  rolle  25514  cmvth  25515  mvth  25516  dvlip  25517  dvlipcn  25518  dvle  25531  dvivthlem1  25532  dvivth  25534  lhop2  25539  dvcnvre  25543  dvfsumle  25545  dvfsumge  25546  dvfsumabs  25547  dvfsumlem2  25551  dvfsum2  25558  ftc2  25568  itgparts  25571  itgsubstlem  25572  itgpowd  25574  aalioulem3  25854  taylthlem2  25893  taylth  25894  efcvx  25968  pige3ALT  26036  dvrelog  26152  advlog  26169  advlogexp  26170  logccv  26178  dvcxp1  26255  loglesqrt  26273  divsqrtsumlem  26491  lgamgulmlem2  26541  logexprlim  26735  logdivsum  27043  log2sumbnd  27054  fdvneggt  33681  fdvnegge  33683  itgexpif  33687  logdivsqrle  33731  gg-cmvth  35250  gg-dvfsumle  35251  gg-dvfsumlem2  35252  ftc2nc  36656  dvreasin  36660  dvreacos  36661  areacirclem1  36662  dvrelog2  41015  dvrelog3  41016  dvrelog2b  41017  dvrelogpow2b  41019  aks4d1p1p6  41024  lhe4.4ex1a  43170  dvcosre  44707  dvcnre  44711  itgsin0pilem1  44745  itgsinexplem1  44749  itgcoscmulx  44764  itgiccshift  44775  itgperiod  44776  itgsbtaddcnst  44777  dirkeritg  44897  dirkercncflem2  44899  fourierdlem28  44930  fourierdlem39  44941  fourierdlem56  44957  fourierdlem57  44958  fourierdlem58  44959  fourierdlem59  44960  fourierdlem60  44961  fourierdlem61  44962  fourierdlem62  44963  fourierdlem68  44969  fourierdlem72  44973  fouriersw  45026  etransclem2  45031  etransclem23  45052  etransclem35  45064  etransclem38  45067  etransclem39  45068  etransclem44  45073  etransclem45  45074  etransclem46  45075  etransclem47  45076