Theorem cnelprrecn 11205

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

Syntax hints:   ∈ wcel 2106  {cpr 4630  ℂcc 11110  ℝcr 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-cnex 11168

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  dvfcn  25432  dvnres  25455  dvexp  25477  dvrecg  25497  dvexp3  25502  dvef  25504  dvsincos  25505  dvlipcn  25518  dv11cn  25525  dvply1  25804  dvtaylp  25889  pserdvlem2  25947  pige3ALT  26036  dvlog  26166  advlogexp  26170  logtayl  26175  dvcxp1  26255  dvcxp2  26256  dvcncxp1  26258  dvatan  26447  efrlim  26481  lgamgulmlem2  26541  logdivsum  27043  log2sumbnd  27054  itgexpif  33687  dvtan  36624  dvasin  36658  dvacos  36659  lcmineqlem7  40986  lcmineqlem8  40987  lcmineqlem12  40991  dvrelogpow2b  41019  aks4d1p1p6  41024  lhe4.4ex1a  43170  expgrowthi  43174  expgrowth  43176  binomcxplemdvbinom  43194  binomcxplemnotnn0  43197  dvsinexp  44706  dvsinax  44708  dvasinbx  44715  dvcosax  44721  dvxpaek  44735  itgsincmulx  44769  fourierdlem56  44957  etransclem46  45075