Theorem cnelprrecn 11248

Description: Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
cnelprrecn	⊢ ℂ ∈ {ℝ, ℂ}

Proof of Theorem cnelprrecn

Step	Hyp	Ref	Expression
1		cnex 11236	. 2 ⊢ ℂ ∈ V
2	1	prid2 4763	1 ⊢ ℂ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2108  {cpr 4628  ℂcc 11153  ℝcr 11154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-cnex 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  dvfcn  25943  dvnres  25967  dvexp  25991  dvrecg  26011  dvexp3  26016  dvef  26018  dvsincos  26019  dvlipcn  26033  dv11cn  26040  dvply1  26325  dvtaylp  26412  pserdvlem2  26472  pige3ALT  26562  dvlog  26693  advlogexp  26697  logtayl  26702  dvcxp1  26782  dvcxp2  26783  dvcncxp1  26785  dvatan  26978  efrlim  27012  efrlimOLD  27013  lgamgulmlem2  27073  logdivsum  27577  log2sumbnd  27588  itgexpif  34621  dvtan  37677  dvasin  37711  dvacos  37712  lcmineqlem7  42036  lcmineqlem8  42037  lcmineqlem12  42041  dvrelogpow2b  42069  aks4d1p1p6  42074  readvrec2  42391  readvrec  42392  lhe4.4ex1a  44348  expgrowthi  44352  expgrowth  44354  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  dvsinexp  45926  dvsinax  45928  dvasinbx  45935  dvcosax  45941  dvxpaek  45955  itgsincmulx  45989  fourierdlem56  46177  etransclem46  46295