Theorem cnelprrecn 10630

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

Syntax hints:   ∈ wcel 2114  {cpr 4569  ℂcc 10535  ℝcr 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-cnex 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  dvfcn  24506  dvnres  24528  dvexp  24550  dvrecg  24570  dvexp3  24575  dvef  24577  dvsincos  24578  dvlipcn  24591  dv11cn  24598  dvply1  24873  dvtaylp  24958  pserdvlem2  25016  pige3ALT  25105  dvlog  25234  advlogexp  25238  logtayl  25243  dvcxp1  25321  dvcxp2  25322  dvcncxp1  25324  dvatan  25513  efrlim  25547  lgamgulmlem2  25607  logdivsum  26109  log2sumbnd  26120  itgexpif  31877  dvtan  34957  dvasin  34993  dvacos  34994  lhe4.4ex1a  40681  expgrowthi  40685  expgrowth  40687  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  dvsinexp  42215  dvsinax  42217  dvasinbx  42225  dvcosax  42231  dvxpaek  42245  itgsincmulx  42279  fourierdlem56  42467  etransclem46  42585