Theorem reelprrecn 10707

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 10706	. 2 ⊢ ℝ ∈ V
2	1	prid1 4653	1 ⊢ ℝ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2114  {cpr 4518  ℂcc 10613  ℝcr 10614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-cnex 10671  ax-resscn 10672

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519

This theorem is referenced by:  dvf  24659  dvmptresicc  24668  dvmptcj  24720  dvmptre  24721  dvmptim  24722  rolle  24742  cmvth  24743  mvth  24744  dvlip  24745  dvlipcn  24746  dvle  24759  dvivthlem1  24760  dvivth  24762  lhop2  24767  dvcnvre  24771  dvfsumle  24773  dvfsumge  24774  dvfsumabs  24775  dvfsumlem2  24779  dvfsum2  24786  ftc2  24796  itgparts  24799  itgsubstlem  24800  itgpowd  24802  aalioulem3  25082  taylthlem2  25121  taylth  25122  efcvx  25196  pige3ALT  25264  dvrelog  25380  advlog  25397  advlogexp  25398  logccv  25406  dvcxp1  25481  loglesqrt  25499  divsqrtsumlem  25717  lgamgulmlem2  25767  logexprlim  25961  logdivsum  26269  log2sumbnd  26280  fdvneggt  32150  fdvnegge  32152  itgexpif  32156  logdivsqrle  32200  ftc2nc  35482  dvreasin  35486  dvreacos  35487  areacirclem1  35488  dvrelog2  39691  dvrelog3  39692  dvrelog2b  39693  dvrelogpow2b  39695  aks4d1p1p6  39700  lhe4.4ex1a  41485  dvcosre  42995  dvcnre  42999  itgsin0pilem1  43033  itgsinexplem1  43037  itgcoscmulx  43052  itgiccshift  43063  itgperiod  43064  itgsbtaddcnst  43065  dirkeritg  43185  dirkercncflem2  43187  fourierdlem28  43218  fourierdlem39  43229  fourierdlem56  43245  fourierdlem57  43246  fourierdlem58  43247  fourierdlem59  43248  fourierdlem60  43249  fourierdlem61  43250  fourierdlem62  43251  fourierdlem68  43257  fourierdlem72  43261  fouriersw  43314  etransclem2  43319  etransclem23  43340  etransclem35  43352  etransclem38  43355  etransclem39  43356  etransclem44  43361  etransclem45  43362  etransclem46  43363  etransclem47  43364