Theorem reelprrecn 10028

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	⊢ ℝ ∈ {ℝ, ℂ}

Proof of Theorem reelprrecn

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

Syntax hints:   ∈ wcel 1990  {cpr 4179  ℂcc 9934  ℝcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-sn 4178  df-pr 4180

This theorem is referenced by:  dvf  23671  dvmptcj  23731  dvmptre  23732  dvmptim  23733  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  dvle  23770  dvivthlem1  23771  dvivth  23773  lhop2  23778  dvcnvre  23782  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem2  23790  dvfsum2  23797  ftc2  23807  itgparts  23810  itgsubstlem  23811  aalioulem3  24089  taylthlem2  24128  taylth  24129  efcvx  24203  pige3  24269  dvrelog  24383  advlog  24400  advlogexp  24401  logccv  24409  dvcxp1  24481  loglesqrt  24499  divsqrtsumlem  24706  lgamgulmlem2  24756  logexprlim  24950  logdivsum  25222  log2sumbnd  25233  fdvneggt  30678  fdvnegge  30680  itgexpif  30684  logdivsqrle  30728  ftc2nc  33494  dvreasin  33498  dvreacos  33499  areacirclem1  33500  itgpowd  37800  lhe4.4ex1a  38528  dvcosre  40126  dvcnre  40130  dvmptresicc  40134  itgsin0pilem1  40165  itgsinexplem1  40169  itgcoscmulx  40185  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  dirkeritg  40319  dirkercncflem2  40321  fourierdlem28  40352  fourierdlem39  40363  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem68  40391  fourierdlem72  40395  fouriersw  40448  etransclem2  40453  etransclem23  40474  etransclem35  40486  etransclem38  40489  etransclem39  40490  etransclem44  40495  etransclem45  40496  etransclem46  40497  etransclem47  40498