Theorem cnelprrecn 10029

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

Syntax hints:   e. wcel 1990   {cpr 4179   CCcc 9934   RRcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  dvfcn  23672  dvnres  23694  dvexp  23716  dvrecg  23736  dvexp3  23741  dvef  23743  dvsincos  23744  dvlipcn  23757  dv11cn  23764  dvply1  24039  dvtaylp  24124  pserdvlem2  24182  pige3  24269  dvlog  24397  advlogexp  24401  logtayl  24406  dvcxp1  24481  dvcxp2  24482  dvcncxp1  24484  dvatan  24662  efrlim  24696  lgamgulmlem2  24756  logdivsum  25222  log2sumbnd  25233  itgexpif  30684  dvtan  33460  dvasin  33496  dvacos  33497  lhe4.4ex1a  38528  expgrowthi  38532  expgrowth  38534  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  dvsinexp  40125  dvsinax  40127  dvasinbx  40135  dvcosax  40141  dvxpaek  40155  itgsincmulx  40190  fourierdlem56  40379  etransclem46  40497