Theorem cnelprrecn 11300

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

This proof depends on syntax axioms:   ∈ wcel 2144  {cpr 4586  ℂcc 11205  ℝcr 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-cnex 11263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-pr 4587

This theorem is used by:  dvfcn  26237  dvnres  26260  dvexp  26282  dvrecg  26302  dvexp3  26307  dvef  26309  dvsincos  26310  dvlipcn  26323  dv11cn  26330  dvply1  26614  dvtaylp  26706  pserdvlem2  26764  pige3ALT  26857  dvlog  26988  advlogexp  26992  logtayl  26997  dvcxp1  27077  dvcxp2  27078  dvcncxp1  27080  dvatan  27272  efrlim  27306  lgamgulmlem2  27366  logdivsum  27869  log2sumbnd  27880  itgexpif  35285  dvtan  38725  dvasin  38759  dvacos  38760  lcmineqlem7  43222  lcmineqlem8  43223  lcmineqlem12  43227  dvrelogpow2b  43255  aks4d1p1p6  43260  readvrec2  43549  readvrec  43550  lhe4.4ex1a  45450  expgrowthi  45454  expgrowth  45456  binomcxplemdvbinom  45474  binomcxplemnotnn0  45477  dvsinexp  47057  dvsinax  47059  dvasinbx  47066  dvcosax  47072  dvxpaek  47086  itgsincmulx  47120  fourierdlem56  47308  etransclem46  47426  dvsec  51067  dvcsc  51068  dvcot  51069