Theorem cnelprrecn 11102

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

Syntax hints:   ∈ wcel 2109  {cpr 4579  ℂcc 11007  ℝcr 11008

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-cnex 11065

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580

This theorem is referenced by:  dvfcn  25807  dvnres  25831  dvexp  25855  dvrecg  25875  dvexp3  25880  dvef  25882  dvsincos  25883  dvlipcn  25897  dv11cn  25904  dvply1  26189  dvtaylp  26276  pserdvlem2  26336  pige3ALT  26427  dvlog  26558  advlogexp  26562  logtayl  26567  dvcxp1  26647  dvcxp2  26648  dvcncxp1  26650  dvatan  26843  efrlim  26877  efrlimOLD  26878  lgamgulmlem2  26938  logdivsum  27442  log2sumbnd  27453  itgexpif  34574  dvtan  37650  dvasin  37684  dvacos  37685  lcmineqlem7  42008  lcmineqlem8  42009  lcmineqlem12  42013  dvrelogpow2b  42041  aks4d1p1p6  42046  readvrec2  42334  readvrec  42335  lhe4.4ex1a  44302  expgrowthi  44306  expgrowth  44308  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  dvsinexp  45892  dvsinax  45894  dvasinbx  45901  dvcosax  45907  dvxpaek  45921  itgsincmulx  45955  fourierdlem56  46143  etransclem46  46261