Theorem cnelprrecn 9908

Description: Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
cnelprrecn	⊢ ℂ ∈ {ℝ, ℂ}

Proof of Theorem cnelprrecn

Step	Hyp	Ref	Expression
1		cnex 9896	. 2 ⊢ ℂ ∈ V
2	1	prid2 4242	1 ⊢ ℂ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 1977  {cpr 4127  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-cnex 9871

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  dvfcn  23478  dvnres  23500  dvexp  23522  dvexp3  23545  dvef  23547  dvsincos  23548  dvlipcn  23561  dv11cn  23568  dvply1  23843  dvtaylp  23928  pserdvlem2  23986  pige3  24073  dvlog  24197  advlogexp  24201  logtayl  24206  dvcxp1  24281  dvcxp2  24282  dvcncxp1  24284  dvatan  24462  efrlim  24496  lgamgulmlem2  24556  logdivsum  25022  log2sumbnd  25033  dvtan  32630  dvasin  32666  dvacos  32667  lhe4.4ex1a  37550  expgrowthi  37554  expgrowth  37556  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  dvsinexp  38798  dvrecg  38800  dvsinax  38801  dvasinbx  38810  dvcosax  38816  dvxpaek  38830  itgsincmulx  38866  fourierdlem56  39055  etransclem46  39173