Theorem cnelprrecn 11161

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

Syntax hints:   ∈ wcel 2109  {cpr 4591  ℂcc 11066  ℝcr 11067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-cnex 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  dvfcn  25809  dvnres  25833  dvexp  25857  dvrecg  25877  dvexp3  25882  dvef  25884  dvsincos  25885  dvlipcn  25899  dv11cn  25906  dvply1  26191  dvtaylp  26278  pserdvlem2  26338  pige3ALT  26429  dvlog  26560  advlogexp  26564  logtayl  26569  dvcxp1  26649  dvcxp2  26650  dvcncxp1  26652  dvatan  26845  efrlim  26879  efrlimOLD  26880  lgamgulmlem2  26940  logdivsum  27444  log2sumbnd  27455  itgexpif  34597  dvtan  37664  dvasin  37698  dvacos  37699  lcmineqlem7  42023  lcmineqlem8  42024  lcmineqlem12  42028  dvrelogpow2b  42056  aks4d1p1p6  42061  readvrec2  42349  readvrec  42350  lhe4.4ex1a  44318  expgrowthi  44322  expgrowth  44324  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  dvsinexp  45909  dvsinax  45911  dvasinbx  45918  dvcosax  45924  dvxpaek  45938  itgsincmulx  45972  fourierdlem56  46160  etransclem46  46278