Theorem reelprrecn 11217

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4586  ℂcc 11123  ℝcr 11124

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  dvf  26135  dvmptresicc  26144  dvmptcj  26196  dvmptre  26197  dvmptim  26198  rolle  26218  cmvth  26219  mvth  26220  dvlip  26221  dvlipcn  26222  dvle  26235  dvivthlem1  26236  dvivth  26238  lhop2  26243  dvcnvre  26247  dvfsumle  26249  dvfsumge  26250  dvfsumabs  26251  dvfsumlem2  26255  dvfsum2  26262  ftc2  26272  itgparts  26275  itgsubstlem  26276  itgpowd  26278  aalioulem3  26571  taylthlem2  26611  taylth  26612  efcvx  26686  pige3ALT  26758  dvrelog  26875  advlog  26892  advlogexp  26893  logccv  26901  dvcxp1  26978  loglesqrt  26999  divsqrtsumlem  27217  lgamgulmlem2  27267  logexprlim  27462  logdivsum  27770  log2sumbnd  27781  fdvneggt  35109  fdvnegge  35111  itgexpif  35115  logdivsqrle  35159  ftc2nc  38452  dvreasin  38456  dvreacos  38457  areacirclem1  38458  dvrelog2  42931  dvrelog3  42932  dvrelog2b  42933  dvrelogpow2b  42935  aks4d1p1p6  42940  redvmptabs  43236  readvrec2  43237  readvrec  43238  readvcot  43240  lhe4.4ex1a  45154  dvcosre  46741  dvcnre  46745  itgsin0pilem1  46779  itgsinexplem1  46783  itgcoscmulx  46798  itgiccshift  46809  itgperiod  46810  itgsbtaddcnst  46811  dirkeritg  46931  dirkercncflem2  46933  fourierdlem28  46964  fourierdlem39  46975  fourierdlem56  46991  fourierdlem57  46992  fourierdlem58  46993  fourierdlem59  46994  fourierdlem60  46995  fourierdlem61  46996  fourierdlem62  46997  fourierdlem68  47003  fourierdlem72  47007  fouriersw  47060  etransclem2  47065  etransclem23  47086  etransclem35  47098  etransclem38  47101  etransclem39  47102  etransclem44  47107  etransclem45  47108  etransclem46  47109  etransclem47  47110