Theorem reelprrecn 11121

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

Syntax hints:   ∈ wcel 2119  {cpr 4557  ℂcc 11027  ℝcr 11028

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-in 3890  df-ss 3900  df-sn 4556  df-pr 4558

This theorem is referenced by:  dvf  25892  dvmptresicc  25901  dvmptcj  25953  dvmptre  25954  dvmptim  25955  rolle  25975  cmvth  25976  mvth  25977  dvlip  25978  dvlipcn  25979  dvle  25992  dvivthlem1  25993  dvivth  25995  lhop2  26000  dvcnvre  26004  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  dvfsumlem2  26012  dvfsum2  26019  ftc2  26029  itgparts  26032  itgsubstlem  26033  itgpowd  26035  aalioulem3  26318  taylthlem2  26357  taylth  26358  efcvx  26432  pige3ALT  26502  dvrelog  26619  advlog  26636  advlogexp  26637  logccv  26645  dvcxp1  26722  loglesqrt  26743  divsqrtsumlem  26961  lgamgulmlem2  27011  logexprlim  27206  logdivsum  27514  log2sumbnd  27525  fdvneggt  34784  fdvnegge  34786  itgexpif  34790  logdivsqrle  34834  ftc2nc  38069  dvreasin  38073  dvreacos  38074  areacirclem1  38075  dvrelog2  42549  dvrelog3  42550  dvrelog2b  42551  dvrelogpow2b  42553  aks4d1p1p6  42558  redvmptabs  42837  readvrec2  42838  readvrec  42839  readvcot  42841  lhe4.4ex1a  44773  dvcosre  46355  dvcnre  46359  itgsin0pilem1  46393  itgsinexplem1  46397  itgcoscmulx  46412  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  dirkeritg  46545  dirkercncflem2  46547  fourierdlem28  46578  fourierdlem39  46589  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem60  46609  fourierdlem61  46610  fourierdlem62  46611  fourierdlem68  46617  fourierdlem72  46621  fouriersw  46674  etransclem2  46679  etransclem23  46700  etransclem35  46712  etransclem38  46715  etransclem39  46716  etransclem44  46721  etransclem45  46722  etransclem46  46723  etransclem47  46724