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

Theorem cnelprrecn 9886
Description: Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
cnelprrecn ℂ ∈ {ℝ, ℂ}

Proof of Theorem cnelprrecn
StepHypRef Expression
1 cnex 9874 . 2 ℂ ∈ V
21prid2 4241 1 ℂ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  {cpr 4126  cc 9791  cr 9792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-cnex 9849
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127
This theorem is referenced by:  dvfcn  23423  dvnres  23445  dvexp  23467  dvexp3  23490  dvef  23492  dvsincos  23493  dvlipcn  23506  dv11cn  23513  dvply1  23788  dvtaylp  23873  pserdvlem2  23931  pige3  24018  dvlog  24142  advlogexp  24146  logtayl  24151  dvcxp1  24226  dvcxp2  24227  dvcncxp1  24229  dvatan  24407  efrlim  24441  lgamgulmlem2  24501  logdivsum  24967  log2sumbnd  24978  dvtan  32454  dvasin  32490  dvacos  32491  lhe4.4ex1a  37374  expgrowthi  37378  expgrowth  37380  binomcxplemdvbinom  37398  binomcxplemnotnn0  37401  dvsinexp  38622  dvrecg  38624  dvsinax  38625  dvasinbx  38634  dvcosax  38640  dvxpaek  38654  itgsincmulx  38690  fourierdlem56  38879  etransclem46  38997
  Copyright terms: Public domain W3C validator