Theorem cnelprrecn 11166

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

Syntax hints:   ∈ wcel 2142  {cpr 4584  ℂcc 11071  ℝcr 11072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-cnex 11129

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-pr 4585

This theorem is referenced by:  dvfcn  25970  dvnres  25993  dvexp  26015  dvrecg  26035  dvexp3  26040  dvef  26042  dvsincos  26043  dvlipcn  26056  dv11cn  26063  dvply1  26348  dvtaylp  26433  pserdvlem2  26491  pige3ALT  26585  dvlog  26716  advlogexp  26720  logtayl  26725  dvcxp1  26805  dvcxp2  26806  dvcncxp1  26808  dvatan  27000  efrlim  27034  lgamgulmlem2  27094  logdivsum  27597  log2sumbnd  27608  itgexpif  34900  dvtan  38169  dvasin  38203  dvacos  38204  lcmineqlem7  42652  lcmineqlem8  42653  lcmineqlem12  42657  dvrelogpow2b  42685  aks4d1p1p6  42690  readvrec2  42970  readvrec  42971  lhe4.4ex1a  44905  expgrowthi  44909  expgrowth  44911  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  dvsinexp  46485  dvsinax  46487  dvasinbx  46494  dvcosax  46500  dvxpaek  46514  itgsincmulx  46548  fourierdlem56  46736  etransclem46  46854