Theorem cnelprrecn 11122

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

Syntax hints:   ∈ wcel 2119  {cpr 4557  ℂcc 11027  ℝcr 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-cnex 11085

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558

This theorem is referenced by:  dvfcn  25893  dvnres  25916  dvexp  25938  dvrecg  25958  dvexp3  25963  dvef  25965  dvsincos  25966  dvlipcn  25979  dv11cn  25986  dvply1  26268  dvtaylp  26353  pserdvlem2  26411  pige3ALT  26502  dvlog  26633  advlogexp  26637  logtayl  26642  dvcxp1  26722  dvcxp2  26723  dvcncxp1  26725  dvatan  26917  efrlim  26951  lgamgulmlem2  27011  logdivsum  27514  log2sumbnd  27525  itgexpif  34790  dvtan  38037  dvasin  38071  dvacos  38072  lcmineqlem7  42520  lcmineqlem8  42521  lcmineqlem12  42525  dvrelogpow2b  42553  aks4d1p1p6  42558  readvrec2  42838  readvrec  42839  lhe4.4ex1a  44773  expgrowthi  44777  expgrowth  44779  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  dvsinexp  46354  dvsinax  46356  dvasinbx  46363  dvcosax  46369  dvxpaek  46383  itgsincmulx  46417  fourierdlem56  46605  etransclem46  46723