Theorem cnelprrecn 9663

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 9651	. 2 |- CC e. _V
2	1	prid2 4094	1 |- CC e. { RR , CC }

Syntax hints:   e. wcel 1898   {cpr 3982   CCcc 9568   RRcr 9569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-cnex 9626

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983

This theorem is referenced by:  dvfcn  22919  dvnres  22941  dvexp  22963  dvexp3  22986  dvef  22988  dvsincos  22989  dvlipcn  23002  dv11cn  23009  dvply1  23293  dvtaylp  23381  pserdvlem2  23439  pige3  23528  dvlog  23652  advlogexp  23656  logtayl  23661  dvcxp1  23736  dvcxp2  23737  dvcncxp1  23739  dvatan  23917  efrlim  23951  lgamgulmlem2  24011  logdivsum  24427  log2sumbnd  24438  dvtan  32038  dvasin  32074  dvacos  32075  lhe4.4ex1a  36723  expgrowthi  36727  expgrowth  36729  binomcxplemdvbinom  36747  binomcxplemnotnn0  36750  dvsinexp  37866  dvrecg  37868  dvsinax  37869  dvasinbx  37878  dvcosax  37884  dvxpaek  37901  itgsincmulx  37937  fourierdlem56  38127  etransclem46  38246