Theorem reelprrecn 10623

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

Syntax hints:   ∈ wcel 2110  {cpr 4562  ℂcc 10529  ℝcr 10530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-cnex 10587  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-sn 4561  df-pr 4563

This theorem is referenced by:  dvf  24499  dvmptcj  24559  dvmptre  24560  dvmptim  24561  rolle  24581  cmvth  24582  mvth  24583  dvlip  24584  dvlipcn  24585  dvle  24598  dvivthlem1  24599  dvivth  24601  lhop2  24606  dvcnvre  24610  dvfsumle  24612  dvfsumge  24613  dvfsumabs  24614  dvfsumlem2  24618  dvfsum2  24625  ftc2  24635  itgparts  24638  itgsubstlem  24639  aalioulem3  24917  taylthlem2  24956  taylth  24957  efcvx  25031  pige3ALT  25099  dvrelog  25214  advlog  25231  advlogexp  25232  logccv  25240  dvcxp1  25315  loglesqrt  25333  divsqrtsumlem  25551  lgamgulmlem2  25601  logexprlim  25795  logdivsum  26103  log2sumbnd  26114  fdvneggt  31866  fdvnegge  31868  itgexpif  31872  logdivsqrle  31916  ftc2nc  34970  dvreasin  34974  dvreacos  34975  areacirclem1  34976  itgpowd  39814  lhe4.4ex1a  40654  dvcosre  42189  dvcnre  42193  dvmptresicc  42197  itgsin0pilem1  42228  itgsinexplem1  42232  itgcoscmulx  42247  itgiccshift  42258  itgperiod  42259  itgsbtaddcnst  42260  dirkeritg  42381  dirkercncflem2  42383  fourierdlem28  42414  fourierdlem39  42425  fourierdlem56  42441  fourierdlem57  42442  fourierdlem58  42443  fourierdlem59  42444  fourierdlem60  42445  fourierdlem61  42446  fourierdlem62  42447  fourierdlem68  42453  fourierdlem72  42457  fouriersw  42510  etransclem2  42515  etransclem23  42536  etransclem35  42548  etransclem38  42551  etransclem39  42552  etransclem44  42557  etransclem45  42558  etransclem46  42559  etransclem47  42560