Theorem cnelprrecn 11137

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

Syntax hints:   ∈ wcel 2109  {cpr 4587  ℂcc 11042  ℝcr 11043

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 11100

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 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  dvfcn  25785  dvnres  25809  dvexp  25833  dvrecg  25853  dvexp3  25858  dvef  25860  dvsincos  25861  dvlipcn  25875  dv11cn  25882  dvply1  26167  dvtaylp  26254  pserdvlem2  26314  pige3ALT  26405  dvlog  26536  advlogexp  26540  logtayl  26545  dvcxp1  26625  dvcxp2  26626  dvcncxp1  26628  dvatan  26821  efrlim  26855  efrlimOLD  26856  lgamgulmlem2  26916  logdivsum  27420  log2sumbnd  27431  itgexpif  34570  dvtan  37637  dvasin  37671  dvacos  37672  lcmineqlem7  41996  lcmineqlem8  41997  lcmineqlem12  42001  dvrelogpow2b  42029  aks4d1p1p6  42034  readvrec2  42322  readvrec  42323  lhe4.4ex1a  44291  expgrowthi  44295  expgrowth  44297  binomcxplemdvbinom  44315  binomcxplemnotnn0  44318  dvsinexp  45882  dvsinax  45884  dvasinbx  45891  dvcosax  45897  dvxpaek  45911  itgsincmulx  45945  fourierdlem56  46133  etransclem46  46251