Theorem cnelprrecn 11168

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

Syntax hints:   ∈ wcel 2109  {cpr 4594  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-cnex 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  dvfcn  25816  dvnres  25840  dvexp  25864  dvrecg  25884  dvexp3  25889  dvef  25891  dvsincos  25892  dvlipcn  25906  dv11cn  25913  dvply1  26198  dvtaylp  26285  pserdvlem2  26345  pige3ALT  26436  dvlog  26567  advlogexp  26571  logtayl  26576  dvcxp1  26656  dvcxp2  26657  dvcncxp1  26659  dvatan  26852  efrlim  26886  efrlimOLD  26887  lgamgulmlem2  26947  logdivsum  27451  log2sumbnd  27462  itgexpif  34604  dvtan  37671  dvasin  37705  dvacos  37706  lcmineqlem7  42030  lcmineqlem8  42031  lcmineqlem12  42035  dvrelogpow2b  42063  aks4d1p1p6  42068  readvrec2  42356  readvrec  42357  lhe4.4ex1a  44325  expgrowthi  44329  expgrowth  44331  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  dvsinexp  45916  dvsinax  45918  dvasinbx  45925  dvcosax  45931  dvxpaek  45945  itgsincmulx  45979  fourierdlem56  46167  etransclem46  46285