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

Theorem cnelprrecn 9597
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  |-  CC  e.  { RR ,  CC }

Proof of Theorem cnelprrecn
StepHypRef Expression
1 cnex 9585 . 2  |-  CC  e.  _V
21prid2 4142 1  |-  CC  e.  { RR ,  CC }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   {cpr 4035   CCcc 9502   RRcr 9503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-cnex 9560
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486  df-sn 4034  df-pr 4036
This theorem is referenced by:  dvfcn  22180  dvnres  22202  dvexp  22224  dvexp3  22247  dvef  22249  dvsincos  22250  dvlipcn  22263  dv11cn  22270  dvply1  22547  dvtaylp  22632  pserdvlem2  22690  pige3  22776  dvlog  22898  advlogexp  22902  logtayl  22907  dvcxp1  22982  dvcxp2  22983  dvatan  23132  efrlim  23165  logdivsum  23584  log2sumbnd  23595  lgamgulmlem2  28397  dvtan  29992  dvcncxp1  30027  dvasin  30030  dvacos  30031  lhe4.4ex1a  31158  expgrowthi  31162  expgrowth  31164  dvsinexp  31561  dvcosax  31579  itgsincmulx  31615
  Copyright terms: Public domain W3C validator