Theorem cnelprrecn 11199

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

Syntax hints:   ∈ wcel 2107  {cpr 4629  ℂcc 11104  ℝcr 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-cnex 11162

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  dvfcn  25407  dvnres  25430  dvexp  25452  dvrecg  25472  dvexp3  25477  dvef  25479  dvsincos  25480  dvlipcn  25493  dv11cn  25500  dvply1  25779  dvtaylp  25864  pserdvlem2  25922  pige3ALT  26011  dvlog  26141  advlogexp  26145  logtayl  26150  dvcxp1  26228  dvcxp2  26229  dvcncxp1  26231  dvatan  26420  efrlim  26454  lgamgulmlem2  26514  logdivsum  27016  log2sumbnd  27027  itgexpif  33556  dvtan  36476  dvasin  36510  dvacos  36511  lcmineqlem7  40838  lcmineqlem8  40839  lcmineqlem12  40843  dvrelogpow2b  40871  aks4d1p1p6  40876  lhe4.4ex1a  43021  expgrowthi  43025  expgrowth  43027  binomcxplemdvbinom  43045  binomcxplemnotnn0  43048  dvsinexp  44562  dvsinax  44564  dvasinbx  44571  dvcosax  44577  dvxpaek  44591  itgsincmulx  44625  fourierdlem56  44813  etransclem46  44931