Theorem n0i 3775

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

Assertion

Ref	Expression
n0i	|- ( B e. A -> -. A = (/) )

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		noel 3774	. . 3 |- -. B e. (/)
2		eleq2 2516	. . 3 |- ( A = (/) -> ( B e. A <-> B e. (/) ) )
3	1, 2	mtbiri 303	. 2 |- ( A = (/) -> -. B e. A )
4	3	con2i 120	1 |- ( B e. A -> -. A = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1383   e. wcel 1804   (/)c0 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-nul 3771

This theorem is referenced by:  ne0i  3776  oprcl  4227  disjss3  4436  iin0  4611  snsn0non  4986  isomin  6218  ovrcl  6314  tfrlem16  7064  oalimcl  7211  omlimcl  7229  oaabs2  7296  ecexr  7318  elpmi  7439  elmapex  7441  pmresg  7448  pmsspw  7455  ixpssmap2g  7500  ixpssmapg  7501  resixpfo  7509  php3  7705  cantnfp1lem2  8101  cantnflem1  8111  cantnfp1lem2OLD  8127  cantnflem1OLD  8134  cnfcom2lem  8148  cnfcom2lemOLD  8156  rankxplim2  8301  rankxplim3  8302  cardlim  8356  alephnbtwn  8455  pwcdadom  8599  ttukeylem5  8896  r1wunlim  9118  nnunb  10797  ssnn0fi  12073  ruclem13  13852  ramtub  14407  elbasfv  14556  elbasov  14557  restsspw  14706  homarcl  15229  grpidval  15761  odlem2  16437  efgrelexlema  16641  subcmn  16719  dvdsrval  17168  pf1rcl  18259  elocv  18572  matrcl  18787  0top  19358  ppttop  19381  pptbas  19382  restrcl  19531  ssrest  19550  iscnp2  19613  lmmo  19754  zfbas  20270  rnelfmlem  20326  isfcls  20383  isnghm  21103  iscau2  21589  itg2cnlem1  22041  itgsubstlem  22322  dchrrcl  23387  eleenn  24071  nbgranself2  24308  uvtxisvtx  24362  uvtx01vtx  24364  2spot0  24936  hon0  26584  dmadjrnb  26697  eulerpartlemgvv  28188  indispcon  28552  cvmtop1  28578  cvmtop2  28579  mrsub0  28749  mrsubf  28750  mrsubccat  28751  mrsubcn  28752  mrsubco  28754  mrsubvrs  28755  msubf  28765  mclsrcl  28794  funpartlem  29567  tailfb  30170  mapco2g  30621  wepwsolem  30962  ssfiunibd  31458  bnj98  33658  atbase  34754  llnbase  34973  lplnbase  34998  lvolbase  35042  osumcllem4N  35423  pexmidlem1N  35434  lhpbase  35462