Theorem reelprrecn 10963

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

Syntax hints:   ∈ wcel 2106  {cpr 4563  ℂcc 10869  ℝcr 10870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564

This theorem is referenced by:  dvf  25071  dvmptresicc  25080  dvmptcj  25132  dvmptre  25133  dvmptim  25134  rolle  25154  cmvth  25155  mvth  25156  dvlip  25157  dvlipcn  25158  dvle  25171  dvivthlem1  25172  dvivth  25174  lhop2  25179  dvcnvre  25183  dvfsumle  25185  dvfsumge  25186  dvfsumabs  25187  dvfsumlem2  25191  dvfsum2  25198  ftc2  25208  itgparts  25211  itgsubstlem  25212  itgpowd  25214  aalioulem3  25494  taylthlem2  25533  taylth  25534  efcvx  25608  pige3ALT  25676  dvrelog  25792  advlog  25809  advlogexp  25810  logccv  25818  dvcxp1  25893  loglesqrt  25911  divsqrtsumlem  26129  lgamgulmlem2  26179  logexprlim  26373  logdivsum  26681  log2sumbnd  26692  fdvneggt  32580  fdvnegge  32582  itgexpif  32586  logdivsqrle  32630  ftc2nc  35859  dvreasin  35863  dvreacos  35864  areacirclem1  35865  dvrelog2  40072  dvrelog3  40073  dvrelog2b  40074  dvrelogpow2b  40076  aks4d1p1p6  40081  lhe4.4ex1a  41947  dvcosre  43453  dvcnre  43457  itgsin0pilem1  43491  itgsinexplem1  43495  itgcoscmulx  43510  itgiccshift  43521  itgperiod  43522  itgsbtaddcnst  43523  dirkeritg  43643  dirkercncflem2  43645  fourierdlem28  43676  fourierdlem39  43687  fourierdlem56  43703  fourierdlem57  43704  fourierdlem58  43705  fourierdlem59  43706  fourierdlem60  43707  fourierdlem61  43708  fourierdlem62  43709  fourierdlem68  43715  fourierdlem72  43719  fouriersw  43772  etransclem2  43777  etransclem23  43798  etransclem35  43810  etransclem38  43813  etransclem39  43814  etransclem44  43819  etransclem45  43820  etransclem46  43821  etransclem47  43822