Theorem cnelprrecn 10895

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

Syntax hints:   ∈ wcel 2108  {cpr 4560  ℂcc 10800  ℝcr 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  dvfcn  24977  dvnres  25000  dvexp  25022  dvrecg  25042  dvexp3  25047  dvef  25049  dvsincos  25050  dvlipcn  25063  dv11cn  25070  dvply1  25349  dvtaylp  25434  pserdvlem2  25492  pige3ALT  25581  dvlog  25711  advlogexp  25715  logtayl  25720  dvcxp1  25798  dvcxp2  25799  dvcncxp1  25801  dvatan  25990  efrlim  26024  lgamgulmlem2  26084  logdivsum  26586  log2sumbnd  26597  itgexpif  32486  dvtan  35754  dvasin  35788  dvacos  35789  lcmineqlem7  39971  lcmineqlem8  39972  lcmineqlem12  39976  dvrelogpow2b  40004  aks4d1p1p6  40009  lhe4.4ex1a  41836  expgrowthi  41840  expgrowth  41842  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  dvsinexp  43342  dvsinax  43344  dvasinbx  43351  dvcosax  43357  dvxpaek  43371  itgsincmulx  43405  fourierdlem56  43593  etransclem46  43711