Theorem ne0ii 3791

Description: If a set has elements, then it is not empty. Inference associated with ne0i 3790. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
ne0ii.1

Assertion

Ref	Expression
ne0ii

Proof of Theorem ne0ii

Step	Hyp	Ref	Expression
1		ne0ii.1	. 2
2		ne0i 3790	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1818  =/=wne 2652  c0 3784

This theorem is referenced by:  vn0  3792  prnz  4149  tpnz  4151  onn0  4947  oawordeulem  7222  noinfep  8097  fin23lem31  8744  isfin1-3  8787  omina  9090  rpnnen1lem4  11240  rpnnen1lem5  11241  rexfiuz  13180  caurcvg  13499  caurcvg2  13500  caucvg  13501  infcvgaux1i  13668  divalglem2  14053  pc2dvds  14402  vdwmc2  14497  cnsubglem  18467  cnmsubglem  18480  pmatcollpw3  19285  zfbas  20397  nrginvrcn  21200  lebnumlem3  21463  caun0  21720  cnflduss  21796  cnfldcusp  21797  reust  21813  recusp  21814  nulmbl2  21947  itg2seq  22149  itg2monolem1  22157  c1lip1  22398  aannenlem2  22725  shintcl  26248  chintcl  26250  nmoprepnf  26786  nmfnrepnf  26799  nmcexi  26945  snct  27534  esum0  28060  esumpcvgval  28084  ismblfin  30055  volsupnfl  30059  itg2addnclem  30066  ftc1anc  30098  incsequz  30241  isbnd3  30280  ssbnd  30284  ioodvbdlimc1  31730  ioodvbdlimc2  31732  dvnprodlem3  31745  stirlinglem13  31868  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  2zlidl  32740  bnj906  33988  bj-tagn0  34537  taupi  37698  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-nul 3785