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

Theorem cnelprrecn 9375
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 9363 . 2  |-  CC  e.  _V
21prid2 3984 1  |-  CC  e.  { RR ,  CC }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   {cpr 3879   CCcc 9280   RRcr 9281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-cnex 9338
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-sn 3878  df-pr 3880
This theorem is referenced by:  dvfcn  21383  dvnres  21405  dvexp  21427  dvexp3  21450  dvef  21452  dvsincos  21453  dvlipcn  21466  dv11cn  21473  dvply1  21750  dvtaylp  21835  pserdvlem2  21893  pige3  21979  dvlog  22096  advlogexp  22100  logtayl  22105  dvcxp1  22180  dvcxp2  22181  dvatan  22330  efrlim  22363  logdivsum  22782  log2sumbnd  22793  lgamgulmlem2  27016  dvtan  28442  dvcncxp1  28477  dvasin  28480  dvacos  28481  lhe4.4ex1a  29603  expgrowthi  29607  expgrowth  29609  dvsinexp  29787
  Copyright terms: Public domain W3C validator