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