Theorem cnelprrecn 11119

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

Syntax hints:   ∈ wcel 2113  {cpr 4582  ℂcc 11024  ℝcr 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-cnex 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  dvfcn  25865  dvnres  25889  dvexp  25913  dvrecg  25933  dvexp3  25938  dvef  25940  dvsincos  25941  dvlipcn  25955  dv11cn  25962  dvply1  26247  dvtaylp  26334  pserdvlem2  26394  pige3ALT  26485  dvlog  26616  advlogexp  26620  logtayl  26625  dvcxp1  26705  dvcxp2  26706  dvcncxp1  26708  dvatan  26901  efrlim  26935  efrlimOLD  26936  lgamgulmlem2  26996  logdivsum  27500  log2sumbnd  27511  itgexpif  34763  dvtan  37871  dvasin  37905  dvacos  37906  lcmineqlem7  42289  lcmineqlem8  42290  lcmineqlem12  42294  dvrelogpow2b  42322  aks4d1p1p6  42327  readvrec2  42616  readvrec  42617  lhe4.4ex1a  44570  expgrowthi  44574  expgrowth  44576  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  dvsinexp  46155  dvsinax  46157  dvasinbx  46164  dvcosax  46170  dvxpaek  46184  itgsincmulx  46218  fourierdlem56  46406  etransclem46  46524