Theorem cnelprrecn 11293

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4586  ℂcc 11198  ℝcr 11199

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-cnex 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  dvfcn  26228  dvnres  26251  dvexp  26273  dvrecg  26293  dvexp3  26298  dvef  26300  dvsincos  26301  dvlipcn  26314  dv11cn  26321  dvply1  26605  dvtaylp  26697  pserdvlem2  26755  pige3ALT  26848  dvlog  26979  advlogexp  26983  logtayl  26988  dvcxp1  27068  dvcxp2  27069  dvcncxp1  27071  dvatan  27263  efrlim  27297  lgamgulmlem2  27357  logdivsum  27860  log2sumbnd  27871  itgexpif  35235  dvtan  38588  dvasin  38622  dvacos  38623  lcmineqlem7  43085  lcmineqlem8  43086  lcmineqlem12  43090  dvrelogpow2b  43118  aks4d1p1p6  43123  readvrec2  43412  readvrec  43413  lhe4.4ex1a  45312  expgrowthi  45316  expgrowth  45318  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  dvsinexp  46920  dvsinax  46922  dvasinbx  46929  dvcosax  46935  dvxpaek  46949  itgsincmulx  46983  fourierdlem56  47171  etransclem46  47289  dvsec  50855  dvcsc  50856  dvcot  50857