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

Step	Hyp	Ref	Expression
1		cnex 9363	. 2 |- CC e. _V
2	1	prid2 3984	1 |- CC e. { RR , CC }

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