Theorem cnelprrecn 10701

Description: Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
cnelprrecn	⊢ ℂ ∈ {ℝ, ℂ}

Proof of Theorem cnelprrecn

Step	Hyp	Ref	Expression
1		cnex 10689	. 2 ⊢ ℂ ∈ V
2	1	prid2 4651	1 ⊢ ℂ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2113  {cpr 4515  ℂcc 10606  ℝcr 10607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-cnex 10664

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-sn 4514  df-pr 4516

This theorem is referenced by:  dvfcn  24652  dvnres  24675  dvexp  24697  dvrecg  24717  dvexp3  24722  dvef  24724  dvsincos  24725  dvlipcn  24738  dv11cn  24745  dvply1  25024  dvtaylp  25109  pserdvlem2  25167  pige3ALT  25256  dvlog  25386  advlogexp  25390  logtayl  25395  dvcxp1  25473  dvcxp2  25474  dvcncxp1  25476  dvatan  25665  efrlim  25699  lgamgulmlem2  25759  logdivsum  26261  log2sumbnd  26272  itgexpif  32148  dvtan  35439  dvasin  35473  dvacos  35474  lcmineqlem7  39652  lcmineqlem8  39653  lcmineqlem12  39657  dvrelogpow2b  39684  aks4d1p1p6  39689  lhe4.4ex1a  41469  expgrowthi  41473  expgrowth  41475  binomcxplemdvbinom  41493  binomcxplemnotnn0  41496  dvsinexp  42978  dvsinax  42980  dvasinbx  42987  dvcosax  42993  dvxpaek  43007  itgsincmulx  43041  fourierdlem56  43229  etransclem46  43347