Theorem cnelprrecn 11131

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

Syntax hints:   ∈ wcel 2114  {cpr 4569  ℂcc 11036  ℝcr 11037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  dvfcn  25875  dvnres  25898  dvexp  25920  dvrecg  25940  dvexp3  25945  dvef  25947  dvsincos  25948  dvlipcn  25961  dv11cn  25968  dvply1  26250  dvtaylp  26335  pserdvlem2  26393  pige3ALT  26484  dvlog  26615  advlogexp  26619  logtayl  26624  dvcxp1  26704  dvcxp2  26705  dvcncxp1  26707  dvatan  26899  efrlim  26933  lgamgulmlem2  26993  logdivsum  27496  log2sumbnd  27507  itgexpif  34750  dvtan  37991  dvasin  38025  dvacos  38026  lcmineqlem7  42474  lcmineqlem8  42475  lcmineqlem12  42479  dvrelogpow2b  42507  aks4d1p1p6  42512  readvrec2  42793  readvrec  42794  lhe4.4ex1a  44756  expgrowthi  44760  expgrowth  44762  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  dvsinexp  46339  dvsinax  46341  dvasinbx  46348  dvcosax  46354  dvxpaek  46368  itgsincmulx  46402  fourierdlem56  46590  etransclem46  46708