Theorem reelprrecn 9573

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	|- RR e. { RR , CC }

Proof of Theorem reelprrecn

Step	Hyp	Ref	Expression
1		reex 9572	. 2 |- RR e. _V
2	1	prid1 4128	1 |- RR e. { RR , CC }

Syntax hints:   e. wcel 1762   {cpr 4022   CCcc 9479   RRcr 9480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-cnex 9537  ax-resscn 9538

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-in 3476  df-ss 3483  df-sn 4021  df-pr 4023

This theorem is referenced by:  dvf  22039  dvmptcj  22099  dvmptre  22100  dvmptim  22101  rolle  22119  cmvth  22120  mvth  22121  dvlip  22122  dvlipcn  22123  dvle  22136  dvivthlem1  22137  dvivth  22139  lhop2  22144  dvcnvre  22148  dvfsumle  22150  dvfsumge  22151  dvfsumabs  22152  dvfsumlem2  22156  dvfsum2  22163  ftc2  22173  itgparts  22176  itgsubstlem  22177  aalioulem3  22457  taylthlem2  22496  taylth  22497  efcvx  22571  pige3  22636  dvrelog  22739  advlog  22756  advlogexp  22757  logccv  22765  dvcxp1  22837  loglesqr  22853  divsqrsumlem  23030  logexprlim  23221  logdivsum  23439  log2sumbnd  23450  lgamgulmlem2  28198  ftc2nc  29663  dvreasin  29669  dvreacos  29670  areacirclem1  29671  itgpowd  30776  lhe4.4ex1a  30789  dvcosre  31194  dvmptresicc  31204  itgsin0pilem1  31222  itgsinexplem1  31226  itgcoscmulx  31242  fouriersw  31487