Theorem cnex 11285

Description: Alias for ax-cnex 11260. See also cnexALT 13118. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

Step	Hyp	Ref	Expression
1		ax-cnex 11260	1 ⊢ ℂ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11202

This proof depends on axioms:  ax-cnex 11260

This theorem is used by:  reex  11295  cnelprrecn  11297  pnfex  11366  nnex  12345  zex  12706  qex  13092  mpoaddex  13120  addex  13121  mpomulex  13122  mulex  13123  rlim  15668  rlimf  15674  rlimss  15675  elo12  15700  o1f  15702  o1dm  15703  cnso  16421  cnaddablx  20088  cnaddabl  20089  cnaddid  20090  cnaddinv  20091  cnfldbas  21688  cnfldcj  21693  cnfldds  21696  cnfldfun  21698  cnfldfunALT  21699  cnmsubglem  21742  cnmsgngrp  21891  psgninv  21894  lmbrf  23584  lmfss  23620  lmres  23624  lmcnp  23628  cnmet  25096  cncfval  25215  elcncf  25216  cncfcnvcn  25252  cnheibor  25282  cnlmodlem1  25463  tcphex  25544  tchnmfval  25555  tcphcph  25564  lmmbr2  25586  lmmbrf  25589  iscau2  25604  iscauf  25607  caucfil  25610  cmetcaulem  25615  caussi  25624  causs  25625  lmclimf  25631  mbff  25952  ismbf  25955  ismbfcn  25956  mbfconst  25960  mbfres  25971  mbfimaopn2  25984  cncombf  25985  cnmbf  25986  0plef  25999  0pledm  26000  itg1ge0  26013  mbfi1fseqlem5  26046  itg2addlem  26085  limcfval  26198  limcrcl  26200  ellimc2  26203  limcflf  26207  limcres  26212  limcun  26221  dvfval  26223  dvbss  26227  dvbsss  26228  perfdvf  26229  dvreslem  26235  dvres2lem  26236  dvcnp2  26246  dvnfval  26248  dvnff  26249  dvnf  26253  dvnbss  26254  dvnadd  26255  dvn2bss  26256  dvnres  26257  cpnfval  26258  cpnord  26261  dvaddbr  26264  dvmulbr  26265  dvnfre  26278  dvexp  26279  dvef  26306  c1liplem1  26322  c1lip2  26324  lhop1lem  26339  plyval  26517  elply  26519  elply2  26520  plyf  26522  plyss  26523  elplyr  26525  plyeq0lem  26535  plyeq0  26536  plypf1  26537  plyaddlem1  26538  plymullem1  26539  plyaddlem  26540  plymullem  26541  plysub  26544  coeeulem  26549  coeeq  26552  dgrlem  26554  coeidlem  26562  plyco  26566  coe0  26581  coesub  26582  dgrmulc  26596  dgrsub  26597  dgrcolem1  26598  dgrcolem2  26599  plymul0or  26605  plymul02  26607  plyn0mulidp  26608  dvnply2  26614  plycpn  26616  plydivlem3  26622  plydivlem4  26623  plydiveu  26625  plyremlem  26631  plyrem  26632  facth  26633  fta1lem  26634  rnplynfin  26636  quotcan  26638  vieta1lem2  26640  plyexmo  26642  elqaalem3  26650  qaa  26653  iaaOLD  26658  aannenlem1  26661  aannenlem2  26662  aannenlem3  26663  taylfvallem1  26690  taylfval  26692  tayl0  26695  taylplem1  26696  taylply2  26701  taylply  26702  dvtaylp  26703  dvntaylp  26704  dvntaylp0  26705  taylthlem1  26706  taylthlem2  26707  ulmval  26713  ulmss  26730  ulmcn  26732  mtest  26737  pserulm  26755  psercn  26759  pserdvlem2  26761  abelth  26774  reefgim  26783  cxpcn2  27080  logbmpt  27122  logbfval  27124  lgamgulmlem5  27366  lgamgulmlem6  27367  lgamgulm2  27369  lgamcvglem  27373  ftalem7  27412  dchrfi  27588  cffldtocusgr  30034  isvcOLD  31187  cnaddabloOLD  31189  cnnvg  31286  cnnvs  31288  cnnvnm  31289  cncph  31427  hvmulex  31619  hfsmval  32346  hfmmval  32347  nmfnval  32484  nlfnval  32489  elcnfn  32490  ellnfn  32491  specval  32506  hhcnf  32513  constrsuc  34417  lmlim  34626  esumcvg  34765  signsplypnf  35226  signsply0  35227  breprexplemb  35307  breprexpnat  35310  vtsval  35313  circlemethnat  35317  circlevma  35318  circlemethhgt  35319  cvxpconn  36094  fwddifval  37020  fwddifnval  37021  ivthALT  37216  knoppcnlem5  37456  knoppcnlem8  37459  bj-inftyexpiinv  38223  bj-inftyexpidisj  38225  caures  38788  cntotbnd  38824  cnpwstotbnd  38825  rrnval  38855  cnaddcom  40123  subex  43392  absex  43393  cjex  43394  elmnc  44232  mpaaeu  44246  itgoval  44257  itgocn  44260  rngunsnply  44265  binomcxplemnotnn0  45434  climexp  46711  xlimbr  46931  fuzxrpmcn  46932  xlimmnfvlem2  46937  xlimpnfvlem2  46941  mulcncff  46974  subcncff  46984  addcncff  46988  cncfuni  46990  divcncff  46995  dvsinax  47017  dvcosax  47030  dvnmptdivc  47042  dvnmptconst  47045  dvnxpaek  47046  dvnmul  47047  dvnprodlem3  47052  etransclem1  47339  etransclem2  47340  etransclem4  47342  etransclem13  47351  etransclem46  47384  sqrtnnaa  48007  sqrtnzqaa  48008  numtowerdt  48010  cjnpoly  48033  fdivpm  49749  amgmlemALT  51157