Theorem reelprrecn 10629

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

Syntax hints:   ∈ wcel 2114  {cpr 4569  ℂcc 10535  ℝcr 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570

This theorem is referenced by:  dvf  24505  dvmptcj  24565  dvmptre  24566  dvmptim  24567  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dvle  24604  dvivthlem1  24605  dvivth  24607  lhop2  24612  dvcnvre  24616  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  dvfsum2  24631  ftc2  24641  itgparts  24644  itgsubstlem  24645  aalioulem3  24923  taylthlem2  24962  taylth  24963  efcvx  25037  pige3ALT  25105  dvrelog  25220  advlog  25237  advlogexp  25238  logccv  25246  dvcxp1  25321  loglesqrt  25339  divsqrtsumlem  25557  lgamgulmlem2  25607  logexprlim  25801  logdivsum  26109  log2sumbnd  26120  fdvneggt  31871  fdvnegge  31873  itgexpif  31877  logdivsqrle  31921  ftc2nc  34991  dvreasin  34995  dvreacos  34996  areacirclem1  34997  itgpowd  39841  lhe4.4ex1a  40681  dvcosre  42216  dvcnre  42220  dvmptresicc  42224  itgsin0pilem1  42255  itgsinexplem1  42259  itgcoscmulx  42274  itgiccshift  42285  itgperiod  42286  itgsbtaddcnst  42287  dirkeritg  42407  dirkercncflem2  42409  fourierdlem28  42440  fourierdlem39  42451  fourierdlem56  42467  fourierdlem57  42468  fourierdlem58  42469  fourierdlem59  42470  fourierdlem60  42471  fourierdlem61  42472  fourierdlem62  42473  fourierdlem68  42479  fourierdlem72  42483  fouriersw  42536  etransclem2  42541  etransclem23  42562  etransclem35  42574  etransclem38  42577  etransclem39  42578  etransclem44  42583  etransclem45  42584  etransclem46  42585  etransclem47  42586