Theorem cnelprrecn 11099

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 11087	. 2 ⊢ ℂ ∈ V
2	1	prid2 4713	1 ⊢ ℂ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2111  {cpr 4575  ℂcc 11004  ℝcr 11005

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-cnex 11062

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  dvfcn  25836  dvnres  25860  dvexp  25884  dvrecg  25904  dvexp3  25909  dvef  25911  dvsincos  25912  dvlipcn  25926  dv11cn  25933  dvply1  26218  dvtaylp  26305  pserdvlem2  26365  pige3ALT  26456  dvlog  26587  advlogexp  26591  logtayl  26596  dvcxp1  26676  dvcxp2  26677  dvcncxp1  26679  dvatan  26872  efrlim  26906  efrlimOLD  26907  lgamgulmlem2  26967  logdivsum  27471  log2sumbnd  27482  itgexpif  34619  dvtan  37718  dvasin  37752  dvacos  37753  lcmineqlem7  42076  lcmineqlem8  42077  lcmineqlem12  42081  dvrelogpow2b  42109  aks4d1p1p6  42114  readvrec2  42402  readvrec  42403  lhe4.4ex1a  44370  expgrowthi  44374  expgrowth  44376  binomcxplemdvbinom  44394  binomcxplemnotnn0  44397  dvsinexp  45957  dvsinax  45959  dvasinbx  45966  dvcosax  45972  dvxpaek  45986  itgsincmulx  46020  fourierdlem56  46208  etransclem46  46326