Theorem cnelprrecn 11188

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

Syntax hints:   ∈ wcel 2143  {cpr 4591  ℂcc 11093  ℝcr 11094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-cnex 11151

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  dvfcn  26067  dvnres  26090  dvexp  26112  dvrecg  26132  dvexp3  26137  dvef  26139  dvsincos  26140  dvlipcn  26153  dv11cn  26160  dvply1  26445  dvtaylp  26533  pserdvlem2  26591  pige3ALT  26685  dvlog  26816  advlogexp  26820  logtayl  26825  dvcxp1  26905  dvcxp2  26906  dvcncxp1  26908  dvatan  27100  efrlim  27134  lgamgulmlem2  27194  logdivsum  27697  log2sumbnd  27708  itgexpif  34993  dvtan  38321  dvasin  38355  dvacos  38356  lcmineqlem7  42802  lcmineqlem8  42803  lcmineqlem12  42807  dvrelogpow2b  42835  aks4d1p1p6  42840  readvrec2  43122  readvrec  43123  lhe4.4ex1a  45039  expgrowthi  45043  expgrowth  45045  binomcxplemdvbinom  45063  binomcxplemnotnn0  45066  dvsinexp  46625  dvsinax  46627  dvasinbx  46634  dvcosax  46640  dvxpaek  46654  itgsincmulx  46688  fourierdlem56  46876  etransclem46  46994