MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnex Structured version   Unicode version

Theorem cnex 9076
Description: Alias for ax-cnex 9051. See also cnexALT 10613. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex  |-  CC  e.  _V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 9051 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2958   CCcc 8993
This theorem is referenced by:  reex  9086  nnex  10011  zex  10296  qex  10591  addex  10615  mulex  10616  pnfxr  10718  rlim  12294  rlimf  12300  rlimss  12301  elo12  12326  o1f  12328  o1dm  12329  cnso  12851  cnaddablx  15486  cnaddabl  15487  cnfldbas  16712  cnfldcj  16715  cnfldds  16718  cnmsubglem  16766  lmbrf  17329  lmfss  17365  lmres  17369  lmcnp  17373  cnmet  18811  cncfval  18923  elcncf  18924  cncfcnvcn  18956  cnheibor  18985  tchex  19181  tchnmfval  19191  tchcph  19199  lmmbr2  19217  lmmbrf  19220  iscau2  19235  iscauf  19238  caucfil  19241  cmetcaulem  19246  caussi  19255  causs  19256  lmclimf  19261  mbff  19522  ismbf  19525  ismbfcn  19526  mbfconst  19530  mbfres  19539  mbfimaopn2  19552  cncombf  19553  cnmbf  19554  0plef  19567  0pledm  19568  itg1ge0  19581  mbfi1fseqlem5  19614  itg2addlem  19653  limcfval  19764  limcrcl  19766  ellimc2  19769  limcflf  19773  limcres  19778  limcun  19787  dvfval  19789  dvbss  19793  dvbsss  19794  perfdvf  19795  dvfcn  19800  dvreslem  19801  dvres2lem  19802  dvcnp2  19811  dvnfval  19813  dvnff  19814  dvnf  19818  dvnbss  19819  dvnadd  19820  dvn2bss  19821  dvnres  19822  cpnfval  19823  cpnord  19826  dvaddbr  19829  dvmulbr  19830  dvnfre  19843  dvexp  19844  dvexp3  19867  dvef  19869  dvsincos  19870  dvlipcn  19883  c1liplem1  19885  c1lip2  19887  dv11cn  19890  lhop1lem  19902  plyval  20117  elply  20119  elply2  20120  plyf  20122  plyss  20123  elplyr  20125  plyeq0lem  20134  plyeq0  20135  plypf1  20136  plyaddlem1  20137  plymullem1  20138  plyaddlem  20139  plymullem  20140  plysub  20143  coeeulem  20148  coeeq  20151  dgrlem  20153  coeidlem  20161  plyco  20165  coe0  20179  coesub  20180  dgrmulc  20194  dgrsub  20195  dgrcolem1  20196  dgrcolem2  20197  plymul0or  20203  dvply1  20206  dvnply2  20209  plycpn  20211  plydivlem3  20217  plydivlem4  20218  plydiveu  20220  plyremlem  20226  plyrem  20227  facth  20228  fta1lem  20229  quotcan  20231  vieta1lem2  20233  plyexmo  20235  elqaalem3  20243  qaa  20245  iaa  20247  aannenlem1  20250  aannenlem2  20251  aannenlem3  20252  taylfvallem1  20278  taylfval  20280  tayl0  20283  taylplem1  20284  taylply2  20289  taylply  20290  dvtaylp  20291  dvntaylp  20292  dvntaylp0  20293  taylthlem1  20294  taylthlem2  20295  ulmval  20301  ulmss  20318  ulmcn  20320  mtest  20325  pserulm  20343  psercn  20347  pserdvlem2  20349  abelth  20362  reefgim  20371  pige3  20430  dvlog  20547  advlogexp  20551  logtayl  20556  dvcxp1  20631  dvcxp2  20632  cxpcn2  20635  dvatan  20780  efrlim  20813  ftalem7  20866  dchrfi  21044  logdivsum  21232  log2sumbnd  21243  cnaddablo  21943  ablomul  21948  vcoprne  22063  isvc  22065  cnnvg  22174  cnnvs  22177  cnnvnm  22178  cncph  22325  hvmulex  22519  hfsmval  23246  hfmmval  23247  nmfnval  23384  nlfnval  23389  elcnfn  23390  ellnfn  23391  specval  23406  hhcnf  23413  lmlim  24338  esumcvg  24481  lgamgulmlem2  24819  lgamgulmlem5  24822  lgamgulmlem6  24823  lgamgulm2  24825  lgamcvglem  24829  cvxpcon  24934  dvtan  26268  dvreasin  26303  ivthALT  26351  caures  26479  cntotbnd  26518  cnpwstotbnd  26519  rrnval  26549  elmnc  27331  mpaaeu  27345  itgoval  27356  itgocn  27359  rngunsnply  27368  cnmsgngrp  27426  lhe4.4ex1a  27536  expgrowthi  27540  expgrowth  27542  climexp  27720  dvsinexp  27729  cnaddcom  29842
This theorem was proved from axioms:  ax-cnex 9051
  Copyright terms: Public domain W3C validator