Theorem cnelprrecn 11192

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

Syntax hints:   ∈ wcel 2149  {cpr 4596  ℂcc 11097  ℝcr 11098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-cnex 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  dvfcn  26035  dvnres  26058  dvexp  26080  dvrecg  26100  dvexp3  26105  dvef  26107  dvsincos  26108  dvlipcn  26121  dv11cn  26128  dvply1  26413  dvtaylp  26498  pserdvlem2  26556  pige3ALT  26650  dvlog  26781  advlogexp  26785  logtayl  26790  dvcxp1  26870  dvcxp2  26871  dvcncxp1  26873  dvatan  27065  efrlim  27099  lgamgulmlem2  27159  logdivsum  27662  log2sumbnd  27673  itgexpif  34937  dvtan  38208  dvasin  38242  dvacos  38243  lcmineqlem7  42691  lcmineqlem8  42692  lcmineqlem12  42696  dvrelogpow2b  42724  aks4d1p1p6  42729  readvrec2  43011  readvrec  43012  lhe4.4ex1a  44930  expgrowthi  44934  expgrowth  44936  binomcxplemdvbinom  44954  binomcxplemnotnn0  44957  dvsinexp  46516  dvsinax  46518  dvasinbx  46525  dvcosax  46531  dvxpaek  46545  itgsincmulx  46579  fourierdlem56  46767  etransclem46  46885