Theorem cnelprrecn 11203

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

Syntax hints:   ∈ wcel 2107  {cpr 4631  ℂcc 11108  ℝcr 11109

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-cnex 11166

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  dvfcn  25425  dvnres  25448  dvexp  25470  dvrecg  25490  dvexp3  25495  dvef  25497  dvsincos  25498  dvlipcn  25511  dv11cn  25518  dvply1  25797  dvtaylp  25882  pserdvlem2  25940  pige3ALT  26029  dvlog  26159  advlogexp  26163  logtayl  26168  dvcxp1  26248  dvcxp2  26249  dvcncxp1  26251  dvatan  26440  efrlim  26474  lgamgulmlem2  26534  logdivsum  27036  log2sumbnd  27047  itgexpif  33618  dvtan  36538  dvasin  36572  dvacos  36573  lcmineqlem7  40900  lcmineqlem8  40901  lcmineqlem12  40905  dvrelogpow2b  40933  aks4d1p1p6  40938  lhe4.4ex1a  43088  expgrowthi  43092  expgrowth  43094  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  dvsinexp  44627  dvsinax  44629  dvasinbx  44636  dvcosax  44642  dvxpaek  44656  itgsincmulx  44690  fourierdlem56  44878  etransclem46  44996