Theorem cnelprrecn 11332

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

This proof depends on syntax axioms:   ∈ wcel 2147  {cpr 4590  ℂcc 11237  ℝcr 11238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-cnex 11295

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  dvfcn  26283  dvnres  26306  dvexp  26328  dvrecg  26348  dvexp3  26353  dvef  26355  dvsincos  26356  dvlipcn  26369  dv11cn  26376  dvply1  26660  dvtaylp  26754  pserdvlem2  26812  pige3ALT  26905  dvlog  27036  advlogexp  27040  logtayl  27045  dvcxp1  27125  dvcxp2  27126  dvcncxp1  27128  dvatan  27320  efrlim  27354  lgamgulmlem2  27414  logdivsum  27917  log2sumbnd  27928  itgexpif  35346  dvtan  38856  dvasin  38890  dvacos  38891  lcmineqlem7  43351  lcmineqlem8  43352  lcmineqlem12  43356  dvrelogpow2b  43384  aks4d1p1p6  43389  readvrec2  43678  readvrec  43679  lhe4.4ex1a  45574  expgrowthi  45578  expgrowth  45580  binomcxplemdvbinom  45598  binomcxplemnotnn0  45601  dvsinexp  47194  dvsinax  47196  dvasinbx  47203  dvcosax  47209  dvxpaek  47223  itgsincmulx  47257  fourierdlem56  47445  etransclem46  47563  dvsec  51284  dvcsc  51285  dvcot  51286