Theorem cnex 9772

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 1938  Vcvv 3077  ℂcc 9689

This theorem was proved from axioms:  ax-cnex 9747

This theorem is referenced by:  reex  9782  cnelprrecn  9784  nnex  10781  zex  11127  qex  11542  addex  11572  mulex  11573  pnfxr  11691  rlim  13940  rlimf  13946  rlimss  13947  elo12  13972  o1f  13974  o1dm  13975  cnso  14684  cnaddablx  18001  cnaddabl  18002  cnaddid  18003  cnaddinv  18004  cnfldbas  19475  cnfldcj  19478  cnfldds  19481  cnmsubglem  19532  cnmsgngrp  19650  psgninv  19653  lmbrf  20777  lmfss  20813  lmres  20817  lmcnp  20821  cnmet  22294  cncfval  22422  elcncf  22423  cncfcnvcn  22455  cnheibor  22485  tchex  22691  tchnmfval  22702  tchcph  22711  lmmbr2  22729  lmmbrf  22732  iscau2  22747  iscauf  22750  caucfil  22753  cmetcaulem  22758  caussi  22767  causs  22768  lmclimf  22773  mbff  23075  ismbf  23078  ismbfcn  23079  mbfconst  23083  mbfres  23092  mbfimaopn2  23105  cncombf  23106  cnmbf  23107  0plef  23120  0pledm  23121  itg1ge0  23134  mbfi1fseqlem5  23167  itg2addlem  23206  limcfval  23317  limcrcl  23319  ellimc2  23322  limcflf  23326  limcres  23331  limcun  23340  dvfval  23342  dvbss  23346  dvbsss  23347  perfdvf  23348  dvreslem  23354  dvres2lem  23355  dvcnp2  23364  dvnfval  23366  dvnff  23367  dvnf  23371  dvnbss  23372  dvnadd  23373  dvn2bss  23374  dvnres  23375  cpnfval  23376  cpnord  23379  dvaddbr  23382  dvmulbr  23383  dvnfre  23396  dvexp  23397  dvef  23422  c1liplem1  23438  c1lip2  23440  lhop1lem  23455  plyval  23637  elply  23639  elply2  23640  plyf  23642  plyss  23643  elplyr  23645  plyeq0lem  23654  plyeq0  23655  plypf1  23656  plyaddlem1  23657  plymullem1  23658  plyaddlem  23659  plymullem  23660  plysub  23663  coeeulem  23668  coeeq  23671  dgrlem  23673  coeidlem  23681  plyco  23685  coe0  23700  coesub  23701  dgrmulc  23715  dgrsub  23716  dgrcolem1  23717  dgrcolem2  23718  plymul0or  23724  dvnply2  23730  plycpn  23732  plydivlem3  23738  plydivlem4  23739  plydiveu  23741  plyremlem  23747  plyrem  23748  facth  23749  fta1lem  23750  quotcan  23752  vieta1lem2  23754  plyexmo  23756  elqaalem3  23764  elqaalem3OLD  23767  qaa  23769  iaa  23771  aannenlem1  23774  aannenlem2  23775  aannenlem3  23776  taylfvallem1  23802  taylfval  23804  tayl0  23807  taylplem1  23808  taylply2  23813  taylply  23814  dvtaylp  23815  dvntaylp  23816  dvntaylp0  23817  taylthlem1  23818  taylthlem2  23819  ulmval  23825  ulmss  23842  ulmcn  23844  mtest  23849  pserulm  23867  psercn  23871  pserdvlem2  23873  abelth  23886  reefgim  23895  cxpcn2  24174  logbmpt  24213  logbfval  24215  lgamgulmlem5  24446  lgamgulmlem6  24447  lgamgulm2  24449  lgamcvglem  24453  ftalem7  24494  dchrfi  24669  vcoprne  26572  isvc  26574  cnaddablo  26576  cnnvg  26685  cnnvs  26688  cnnvnm  26689  cncph  26836  hvmulex  27040  hfsmval  27769  hfmmval  27770  nmfnval  27907  nlfnval  27912  elcnfn  27913  ellnfn  27914  specval  27929  hhcnf  27936  lmlim  29117  esumcvg  29271  plymul02  29794  plymulx0  29795  signsplypnf  29798  signsply0  29799  cvxpcon  30323  fwddifval  31274  fwddifnval  31275  ivthALT  31334  knoppcnlem5  31491  knoppcnlem8  31494  bj-inftyexpiinv  32103  bj-inftyexpidisj  32105  caures  32616  cntotbnd  32655  cnpwstotbnd  32656  rrnval  32686  cnaddcom  33167  elmnc  36615  mpaaeu  36636  itgoval  36647  itgocn  36650  rngunsnply  36659  binomcxplemnotnn0  37474  climexp  38571  mulcncff  38653  subcncff  38665  addcncff  38670  cncfuni  38672  divcncff  38677  dvsinax  38701  dvcosax  38716  dvnmptdivc  38731  dvnmptconst  38734  dvnxpaek  38735  dvnmul  38736  dvnprodlem3  38741  etransclem1  39034  etransclem2  39035  etransclem4  39037  etransclem13  39046  etransclem46  39079  fdivpm  42240  amgmlemALT  42424