Theorem cnelprrecn 11277

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 11265	. 2 ⊢ ℂ ∈ V
2	1	prid2 4788	1 ⊢ ℂ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2108  {cpr 4650  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  dvfcn  25963  dvnres  25987  dvexp  26011  dvrecg  26031  dvexp3  26036  dvef  26038  dvsincos  26039  dvlipcn  26053  dv11cn  26060  dvply1  26343  dvtaylp  26430  pserdvlem2  26490  pige3ALT  26580  dvlog  26711  advlogexp  26715  logtayl  26720  dvcxp1  26800  dvcxp2  26801  dvcncxp1  26803  dvatan  26996  efrlim  27030  efrlimOLD  27031  lgamgulmlem2  27091  logdivsum  27595  log2sumbnd  27606  itgexpif  34583  dvtan  37630  dvasin  37664  dvacos  37665  lcmineqlem7  41992  lcmineqlem8  41993  lcmineqlem12  41997  dvrelogpow2b  42025  aks4d1p1p6  42030  lhe4.4ex1a  44298  expgrowthi  44302  expgrowth  44304  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  dvsinexp  45832  dvsinax  45834  dvasinbx  45841  dvcosax  45847  dvxpaek  45861  itgsincmulx  45895  fourierdlem56  46083  etransclem46  46201