Theorem cnelprrecn 11208

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

This proof depends on syntax axioms:   ∈ wcel 2146  {cpr 4593  ℂcc 11113  ℝcr 11114

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 2148  ax-9 2156  ax-ext 2737  ax-cnex 11171

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  dvfcn  26118  dvnres  26141  dvexp  26163  dvrecg  26183  dvexp3  26188  dvef  26190  dvsincos  26191  dvlipcn  26204  dv11cn  26211  dvply1  26496  dvtaylp  26584  pserdvlem2  26642  pige3ALT  26736  dvlog  26867  advlogexp  26871  logtayl  26876  dvcxp1  26956  dvcxp2  26957  dvcncxp1  26959  dvatan  27151  efrlim  27185  lgamgulmlem2  27245  logdivsum  27748  log2sumbnd  27759  itgexpif  35058  dvtan  38378  dvasin  38412  dvacos  38413  lcmineqlem7  42860  lcmineqlem8  42861  lcmineqlem12  42865  dvrelogpow2b  42893  aks4d1p1p6  42898  readvrec2  43180  readvrec  43181  lhe4.4ex1a  45097  expgrowthi  45101  expgrowth  45103  binomcxplemdvbinom  45121  binomcxplemnotnn0  45124  dvsinexp  46683  dvsinax  46685  dvasinbx  46692  dvcosax  46698  dvxpaek  46712  itgsincmulx  46746  fourierdlem56  46934  etransclem46  47052