Theorem cnelprrecn 10619

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

Syntax hints:   ∈ wcel 2111  {cpr 4527  ℂcc 10524  ℝcr 10525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-cnex 10582

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  dvfcn  24511  dvnres  24534  dvexp  24556  dvrecg  24576  dvexp3  24581  dvef  24583  dvsincos  24584  dvlipcn  24597  dv11cn  24604  dvply1  24880  dvtaylp  24965  pserdvlem2  25023  pige3ALT  25112  dvlog  25242  advlogexp  25246  logtayl  25251  dvcxp1  25329  dvcxp2  25330  dvcncxp1  25332  dvatan  25521  efrlim  25555  lgamgulmlem2  25615  logdivsum  26117  log2sumbnd  26128  itgexpif  31987  dvtan  35107  dvasin  35141  dvacos  35142  lcmineqlem7  39323  lcmineqlem8  39324  lcmineqlem12  39328  lhe4.4ex1a  41033  expgrowthi  41037  expgrowth  41039  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  dvsinexp  42553  dvsinax  42555  dvasinbx  42562  dvcosax  42568  dvxpaek  42582  itgsincmulx  42616  fourierdlem56  42804  etransclem46  42922