Theorem cnelprrecn 11117

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

Syntax hints:   ∈ wcel 2113  {cpr 4580  ℂcc 11022  ℝcr 11023

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 2706  ax-cnex 11080

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581

This theorem is referenced by:  dvfcn  25863  dvnres  25887  dvexp  25911  dvrecg  25931  dvexp3  25936  dvef  25938  dvsincos  25939  dvlipcn  25953  dv11cn  25960  dvply1  26245  dvtaylp  26332  pserdvlem2  26392  pige3ALT  26483  dvlog  26614  advlogexp  26618  logtayl  26623  dvcxp1  26703  dvcxp2  26704  dvcncxp1  26706  dvatan  26899  efrlim  26933  efrlimOLD  26934  lgamgulmlem2  26994  logdivsum  27498  log2sumbnd  27509  itgexpif  34712  dvtan  37810  dvasin  37844  dvacos  37845  lcmineqlem7  42228  lcmineqlem8  42229  lcmineqlem12  42233  dvrelogpow2b  42261  aks4d1p1p6  42266  readvrec2  42558  readvrec  42559  lhe4.4ex1a  44512  expgrowthi  44516  expgrowth  44518  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  dvsinexp  46097  dvsinax  46099  dvasinbx  46106  dvcosax  46112  dvxpaek  46126  itgsincmulx  46160  fourierdlem56  46348  etransclem46  46466