Theorem cnex 11149

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066

This theorem was proved from axioms:  ax-cnex 11124

This theorem is referenced by:  reex  11159  cnelprrecn  11161  pnfex  11227  nnex  12192  zex  12538  qex  12920  mpoaddex  12947  addex  12948  mpomulex  12949  mulex  12950  rlim  15461  rlimf  15467  rlimss  15468  elo12  15493  o1f  15495  o1dm  15496  cnso  16215  cnaddablx  19798  cnaddabl  19799  cnaddid  19800  cnaddinv  19801  cnfldbas  21268  cnfldcj  21273  cnfldds  21276  cnfldfun  21278  cnfldfunALT  21279  cnfldbasOLD  21283  cnfldcjOLD  21286  cnflddsOLD  21289  cnfldfunOLD  21291  cnfldfunALTOLD  21292  cnmsubglem  21347  cnmsgngrp  21488  psgninv  21491  lmbrf  23147  lmfss  23183  lmres  23187  lmcnp  23191  cnmet  24659  cncfval  24781  elcncf  24782  cncfcnvcn  24819  cnheibor  24854  cnlmodlem1  25036  tcphex  25117  tchnmfval  25128  tcphcph  25137  lmmbr2  25159  lmmbrf  25162  iscau2  25177  iscauf  25180  caucfil  25183  cmetcaulem  25188  caussi  25197  causs  25198  lmclimf  25204  mbff  25526  ismbf  25529  ismbfcn  25530  mbfconst  25534  mbfres  25545  mbfimaopn2  25558  cncombf  25559  cnmbf  25560  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  itg2addlem  25659  limcfval  25773  limcrcl  25775  ellimc2  25778  limcflf  25782  limcres  25787  limcun  25796  dvfval  25798  dvbss  25802  dvbsss  25803  perfdvf  25804  dvreslem  25810  dvres2lem  25811  dvcnp2  25821  dvcnp2OLD  25822  dvnfval  25824  dvnff  25825  dvnf  25829  dvnbss  25830  dvnadd  25831  dvn2bss  25832  dvnres  25833  cpnfval  25834  cpnord  25837  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvnfre  25856  dvexp  25857  dvef  25884  c1liplem1  25901  c1lip2  25903  lhop1lem  25918  plyval  26098  elply  26100  elply2  26101  plyf  26103  plyss  26104  elplyr  26106  plyeq0lem  26115  plyeq0  26116  plypf1  26117  plyaddlem1  26118  plymullem1  26119  plyaddlem  26120  plymullem  26121  plysub  26124  coeeulem  26129  coeeq  26132  dgrlem  26134  coeidlem  26142  plyco  26146  coe0  26161  coesub  26162  dgrmulc  26177  dgrsub  26178  dgrcolem1  26179  dgrcolem2  26180  plymul0or  26188  dvnply2  26195  plycpn  26197  plydivlem3  26203  plydivlem4  26204  plydiveu  26206  plyremlem  26212  plyrem  26213  facth  26214  fta1lem  26215  quotcan  26217  vieta1lem2  26219  plyexmo  26221  elqaalem3  26229  qaa  26231  iaa  26233  aannenlem1  26236  aannenlem2  26237  aannenlem3  26238  taylfvallem1  26264  taylfval  26266  tayl0  26269  taylplem1  26270  taylply2  26275  taylply2OLD  26276  taylply  26277  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmval  26289  ulmss  26306  ulmcn  26308  mtest  26313  pserulm  26331  psercn  26336  pserdvlem2  26338  abelth  26351  reefgim  26360  cxpcn2  26656  logbmpt  26698  logbfval  26700  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvglem  26950  ftalem7  26989  dchrfi  27166  cffldtocusgr  29374  cffldtocusgrOLD  29375  isvcOLD  30508  cnaddabloOLD  30510  cnnvg  30607  cnnvs  30609  cnnvnm  30610  cncph  30748  hvmulex  30940  hfsmval  31667  hfmmval  31668  nmfnval  31805  nlfnval  31810  elcnfn  31811  ellnfn  31812  specval  31827  hhcnf  31834  constrsuc  33728  lmlim  33937  esumcvg  34076  plymul02  34537  plymulx0  34538  signsplypnf  34541  signsply0  34542  breprexplemb  34622  breprexpnat  34625  vtsval  34628  circlemethnat  34632  circlevma  34633  circlemethhgt  34634  cvxpconn  35229  fwddifval  36150  fwddifnval  36151  ivthALT  36323  knoppcnlem5  36485  knoppcnlem8  36488  bj-inftyexpiinv  37196  bj-inftyexpidisj  37198  caures  37754  cntotbnd  37790  cnpwstotbnd  37791  rrnval  37821  cnaddcom  38965  subex  42235  absex  42236  cjex  42237  elmnc  43125  mpaaeu  43139  itgoval  43150  itgocn  43153  rngunsnply  43158  binomcxplemnotnn0  44345  climexp  45603  xlimbr  45825  fuzxrpmcn  45826  xlimmnfvlem2  45831  xlimpnfvlem2  45835  mulcncff  45868  subcncff  45878  addcncff  45882  cncfuni  45884  divcncff  45889  dvsinax  45911  dvcosax  45924  dvnmptdivc  45936  dvnmptconst  45939  dvnxpaek  45940  dvnmul  45941  dvnprodlem3  45946  etransclem1  46233  etransclem2  46234  etransclem4  46236  etransclem13  46245  etransclem46  46278  cjnpoly  46890  fdivpm  48532  amgmlemALT  49792