Theorem cnelprrecn 11218

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

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

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 2732  ax-cnex 11181

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  dvfcn  26136  dvnres  26159  dvexp  26181  dvrecg  26201  dvexp3  26206  dvef  26208  dvsincos  26209  dvlipcn  26222  dv11cn  26229  dvply1  26515  dvtaylp  26607  pserdvlem2  26665  pige3ALT  26758  dvlog  26889  advlogexp  26893  logtayl  26898  dvcxp1  26978  dvcxp2  26979  dvcncxp1  26981  dvatan  27173  efrlim  27207  lgamgulmlem2  27267  logdivsum  27770  log2sumbnd  27781  itgexpif  35115  dvtan  38420  dvasin  38454  dvacos  38455  lcmineqlem7  42902  lcmineqlem8  42903  lcmineqlem12  42907  dvrelogpow2b  42935  aks4d1p1p6  42940  readvrec2  43237  readvrec  43238  lhe4.4ex1a  45154  expgrowthi  45158  expgrowth  45160  binomcxplemdvbinom  45178  binomcxplemnotnn0  45181  dvsinexp  46740  dvsinax  46742  dvasinbx  46749  dvcosax  46755  dvxpaek  46769  itgsincmulx  46803  fourierdlem56  46991  etransclem46  47109  dvsec  50690  dvcsc  50691  dvcot  50692