Theorem cnelprrecn 11222

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

Syntax hints:   ∈ wcel 2108  {cpr 4603  ℂcc 11127  ℝcr 11128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-cnex 11185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  dvfcn  25861  dvnres  25885  dvexp  25909  dvrecg  25929  dvexp3  25934  dvef  25936  dvsincos  25937  dvlipcn  25951  dv11cn  25958  dvply1  26243  dvtaylp  26330  pserdvlem2  26390  pige3ALT  26481  dvlog  26612  advlogexp  26616  logtayl  26621  dvcxp1  26701  dvcxp2  26702  dvcncxp1  26704  dvatan  26897  efrlim  26931  efrlimOLD  26932  lgamgulmlem2  26992  logdivsum  27496  log2sumbnd  27507  itgexpif  34638  dvtan  37694  dvasin  37728  dvacos  37729  lcmineqlem7  42048  lcmineqlem8  42049  lcmineqlem12  42053  dvrelogpow2b  42081  aks4d1p1p6  42086  readvrec2  42404  readvrec  42405  lhe4.4ex1a  44353  expgrowthi  44357  expgrowth  44359  binomcxplemdvbinom  44377  binomcxplemnotnn0  44380  dvsinexp  45940  dvsinax  45942  dvasinbx  45949  dvcosax  45955  dvxpaek  45969  itgsincmulx  46003  fourierdlem56  46191  etransclem46  46309