Theorem cnelprrecn 11125

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

Syntax hints:   ∈ wcel 2114  {cpr 4570  ℂcc 11030  ℝcr 11031

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-cnex 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  dvfcn  25888  dvnres  25911  dvexp  25933  dvrecg  25953  dvexp3  25958  dvef  25960  dvsincos  25961  dvlipcn  25974  dv11cn  25981  dvply1  26263  dvtaylp  26350  pserdvlem2  26409  pige3ALT  26500  dvlog  26631  advlogexp  26635  logtayl  26640  dvcxp1  26720  dvcxp2  26721  dvcncxp1  26723  dvatan  26915  efrlim  26949  efrlimOLD  26950  lgamgulmlem2  27010  logdivsum  27513  log2sumbnd  27524  itgexpif  34769  dvtan  38008  dvasin  38042  dvacos  38043  lcmineqlem7  42491  lcmineqlem8  42492  lcmineqlem12  42496  dvrelogpow2b  42524  aks4d1p1p6  42529  readvrec2  42810  readvrec  42811  lhe4.4ex1a  44777  expgrowthi  44781  expgrowth  44783  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  dvsinexp  46360  dvsinax  46362  dvasinbx  46369  dvcosax  46375  dvxpaek  46389  itgsincmulx  46423  fourierdlem56  46611  etransclem46  46729