Theorem cnelprrecn 10964

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

Syntax hints:   ∈ wcel 2106  {cpr 4563  ℂcc 10869  ℝcr 10870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-cnex 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  dvfcn  25072  dvnres  25095  dvexp  25117  dvrecg  25137  dvexp3  25142  dvef  25144  dvsincos  25145  dvlipcn  25158  dv11cn  25165  dvply1  25444  dvtaylp  25529  pserdvlem2  25587  pige3ALT  25676  dvlog  25806  advlogexp  25810  logtayl  25815  dvcxp1  25893  dvcxp2  25894  dvcncxp1  25896  dvatan  26085  efrlim  26119  lgamgulmlem2  26179  logdivsum  26681  log2sumbnd  26692  itgexpif  32586  dvtan  35827  dvasin  35861  dvacos  35862  lcmineqlem7  40043  lcmineqlem8  40044  lcmineqlem12  40048  dvrelogpow2b  40076  aks4d1p1p6  40081  lhe4.4ex1a  41947  expgrowthi  41951  expgrowth  41953  binomcxplemdvbinom  41971  binomcxplemnotnn0  41974  dvsinexp  43452  dvsinax  43454  dvasinbx  43461  dvcosax  43467  dvxpaek  43481  itgsincmulx  43515  fourierdlem56  43703  etransclem46  43821