MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnelprrecn Structured version   Visualization version   GIF version

Theorem cnelprrecn 10231
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
StepHypRef Expression
1 cnex 10219 . 2 ℂ ∈ V
21prid2 4434 1 ℂ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  {cpr 4318  cc 10136  cr 10137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-cnex 10194
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-pr 4319
This theorem is referenced by:  dvfcn  23892  dvnres  23914  dvexp  23936  dvrecg  23956  dvexp3  23961  dvef  23963  dvsincos  23964  dvlipcn  23977  dv11cn  23984  dvply1  24259  dvtaylp  24344  pserdvlem2  24402  pige3  24490  dvlog  24618  advlogexp  24622  logtayl  24627  dvcxp1  24702  dvcxp2  24703  dvcncxp1  24705  dvatan  24883  efrlim  24917  lgamgulmlem2  24977  logdivsum  25443  log2sumbnd  25454  itgexpif  31024  dvtan  33792  dvasin  33828  dvacos  33829  lhe4.4ex1a  39054  expgrowthi  39058  expgrowth  39060  binomcxplemdvbinom  39078  binomcxplemnotnn0  39081  dvsinexp  40643  dvsinax  40645  dvasinbx  40653  dvcosax  40659  dvxpaek  40673  itgsincmulx  40707  fourierdlem56  40896  etransclem46  41014
  Copyright terms: Public domain W3C validator