Theorem n0i 3789

Description: If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
n0i

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		noel 3788	. . 3
2		eleq2 2530	. . 3
3	1, 2	mtbiri 303	. 2
4	3	con2i 120	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818  c0 3784

This theorem is referenced by:  ne0i  3790  oprcl  4242  disjss3  4451  iin0  4626  snsn0non  5001  isomin  6233  ovrcl  6329  tfrlem16  7081  oalimcl  7228  omlimcl  7246  oaabs2  7313  ecexr  7335  elpmi  7457  elmapex  7459  pmresg  7466  pmsspw  7473  ixpssmap2g  7518  ixpssmapg  7519  resixpfo  7527  php3  7723  cantnfp1lem2  8119  cantnflem1  8129  cantnfp1lem2OLD  8145  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom2lemOLD  8174  rankxplim2  8319  rankxplim3  8320  cardlim  8374  alephnbtwn  8473  pwcdadom  8617  ttukeylem5  8914  r1wunlim  9136  nnunb  10816  ssnn0fi  12094  ruclem13  13975  ramtub  14530  elbasfv  14679  elbasov  14680  restsspw  14829  homarcl  15355  grpidval  15887  odlem2  16563  efgrelexlema  16767  subcmn  16845  dvdsrval  17294  pf1rcl  18385  elocv  18699  matrcl  18914  0top  19485  ppttop  19508  pptbas  19509  restrcl  19658  ssrest  19677  iscnp2  19740  lmmo  19881  zfbas  20397  rnelfmlem  20453  isfcls  20510  isnghm  21230  iscau2  21716  itg2cnlem1  22168  itgsubstlem  22449  dchrrcl  23515  eleenn  24199  nbgranself2  24436  uvtxisvtx  24490  uvtx01vtx  24492  2spot0  25064  hon0  26712  dmadjrnb  26825  eulerpartlemgvv  28315  indispcon  28679  cvmtop1  28705  cvmtop2  28706  mrsub0  28876  mrsubf  28877  mrsubccat  28878  mrsubcn  28879  mrsubco  28881  mrsubvrs  28882  msubf  28892  mclsrcl  28921  funpartlem  29592  tailfb  30195  mapco2g  30646  wepwsolem  30987  ssfiunibd  31509  mptrcl  32555  bnj98  33925  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  osumcllem4N  35683  pexmidlem1N  35694  lhpbase  35722

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-v 3111  df-dif 3478  df-nul 3785