Theorem cnelprrecn 10316

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

Syntax hints:   ∈ wcel 2157  {cpr 4369  ℂcc 10221  ℝcr 10222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776  ax-cnex 10279

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-v 3386  df-un 3773  df-sn 4368  df-pr 4370

This theorem is referenced by:  dvfcn  24010  dvnres  24032  dvexp  24054  dvrecg  24074  dvexp3  24079  dvef  24081  dvsincos  24082  dvlipcn  24095  dv11cn  24102  dvply1  24377  dvtaylp  24462  pserdvlem2  24520  pige3  24608  dvlog  24735  advlogexp  24739  logtayl  24744  dvcxp1  24822  dvcxp2  24823  dvcncxp1  24825  dvatan  25011  efrlim  25045  lgamgulmlem2  25105  logdivsum  25571  log2sumbnd  25582  itgexpif  31197  dvtan  33941  dvasin  33977  dvacos  33978  lhe4.4ex1a  39299  expgrowthi  39303  expgrowth  39305  binomcxplemdvbinom  39323  binomcxplemnotnn0  39326  dvsinexp  40858  dvsinax  40860  dvasinbx  40868  dvcosax  40874  dvxpaek  40888  itgsincmulx  40922  fourierdlem56  41111  etransclem46  41229