Theorem cnex 9896

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ℂcc 9813

This theorem was proved from axioms:  ax-cnex 9871

This theorem is referenced by:  reex  9906  cnelprrecn  9908  pnfxr  9971  nnex  10903  zex  11263  qex  11676  addex  11706  mulex  11707  rlim  14074  rlimf  14080  rlimss  14081  elo12  14106  o1f  14108  o1dm  14109  cnso  14815  cnaddablx  18094  cnaddabl  18095  cnaddid  18096  cnaddinv  18097  cnfldbas  19571  cnfldcj  19574  cnfldds  19577  cnmsubglem  19628  cnmsgngrp  19744  psgninv  19747  lmbrf  20874  lmfss  20910  lmres  20914  lmcnp  20918  cnmet  22385  cncfval  22499  elcncf  22500  cncfcnvcn  22532  cnheibor  22562  cnlmodlem1  22744  tchex  22824  tchnmfval  22835  tchcph  22844  lmmbr2  22865  lmmbrf  22868  iscau2  22883  iscauf  22886  caucfil  22889  cmetcaulem  22894  caussi  22903  causs  22904  lmclimf  22910  mbff  23200  ismbf  23203  ismbfcn  23204  mbfconst  23208  mbfres  23217  mbfimaopn2  23230  cncombf  23231  cnmbf  23232  0plef  23245  0pledm  23246  itg1ge0  23259  mbfi1fseqlem5  23292  itg2addlem  23331  limcfval  23442  limcrcl  23444  ellimc2  23447  limcflf  23451  limcres  23456  limcun  23465  dvfval  23467  dvbss  23471  dvbsss  23472  perfdvf  23473  dvreslem  23479  dvres2lem  23480  dvcnp2  23489  dvnfval  23491  dvnff  23492  dvnf  23496  dvnbss  23497  dvnadd  23498  dvn2bss  23499  dvnres  23500  cpnfval  23501  cpnord  23504  dvaddbr  23507  dvmulbr  23508  dvnfre  23521  dvexp  23522  dvef  23547  c1liplem1  23563  c1lip2  23565  lhop1lem  23580  plyval  23753  elply  23755  elply2  23756  plyf  23758  plyss  23759  elplyr  23761  plyeq0lem  23770  plyeq0  23771  plypf1  23772  plyaddlem1  23773  plymullem1  23774  plyaddlem  23775  plymullem  23776  plysub  23779  coeeulem  23784  coeeq  23787  dgrlem  23789  coeidlem  23797  plyco  23801  coe0  23816  coesub  23817  dgrmulc  23831  dgrsub  23832  dgrcolem1  23833  dgrcolem2  23834  plymul0or  23840  dvnply2  23846  plycpn  23848  plydivlem3  23854  plydivlem4  23855  plydiveu  23857  plyremlem  23863  plyrem  23864  facth  23865  fta1lem  23866  quotcan  23868  vieta1lem2  23870  plyexmo  23872  elqaalem3  23880  qaa  23882  iaa  23884  aannenlem1  23887  aannenlem2  23888  aannenlem3  23889  taylfvallem1  23915  taylfval  23917  tayl0  23920  taylplem1  23921  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulmval  23938  ulmss  23955  ulmcn  23957  mtest  23962  pserulm  23980  psercn  23984  pserdvlem2  23986  abelth  23999  reefgim  24008  cxpcn2  24287  logbmpt  24326  logbfval  24328  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvglem  24566  ftalem7  24605  dchrfi  24780  isvcOLD  26818  cnaddabloOLD  26820  cnnvg  26917  cnnvs  26919  cnnvnm  26920  cncph  27058  hvmulex  27252  hfsmval  27981  hfmmval  27982  nmfnval  28119  nlfnval  28124  elcnfn  28125  ellnfn  28126  specval  28141  hhcnf  28148  lmlim  29321  esumcvg  29475  plymul02  29949  plymulx0  29950  signsplypnf  29953  signsply0  29954  cvxpcon  30478  fwddifval  31439  fwddifnval  31440  ivthALT  31500  knoppcnlem5  31657  knoppcnlem8  31660  bj-inftyexpiinv  32272  bj-inftyexpidisj  32274  caures  32726  cntotbnd  32765  cnpwstotbnd  32766  rrnval  32796  cnaddcom  33277  elmnc  36725  mpaaeu  36739  itgoval  36750  itgocn  36753  rngunsnply  36762  binomcxplemnotnn0  37577  climexp  38672  mulcncff  38753  subcncff  38765  addcncff  38770  cncfuni  38772  divcncff  38777  dvsinax  38801  dvcosax  38816  dvnmptdivc  38828  dvnmptconst  38831  dvnxpaek  38832  dvnmul  38833  dvnprodlem3  38838  etransclem1  39128  etransclem2  39129  etransclem4  39131  etransclem13  39140  etransclem46  39173  fdivpm  42135  amgmlemALT  42358