Theorem n0i 3783

Description: If a set has elements, 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 3782	. . 3 |- -. B e. (/)
2		eleq2 2533	. . 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 1374   e. wcel 1762   (/)c0 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-dif 3472  df-nul 3779

This theorem is referenced by:  ne0i  3784  oprcl  4231  disjss3  4439  iin0  4614  snsn0non  4989  isomin  6212  ovrcl  6305  tfrlem16  7052  oalimcl  7199  omlimcl  7217  oaabs2  7284  ecexr  7306  elpmi  7427  elmapex  7429  pmresg  7436  pmsspw  7443  ixpssmap2g  7488  ixpssmapg  7489  resixpfo  7497  php3  7693  cantnfp1lem2  8087  cantnflem1  8097  cantnfp1lem2OLD  8113  cantnflem1OLD  8120  cnfcom2lem  8134  cnfcom2lemOLD  8142  rankxplim2  8287  rankxplim3  8288  cardlim  8342  alephnbtwn  8441  pwcdadom  8585  ttukeylem5  8882  r1wunlim  9104  nnunb  10780  ssnn0fi  12050  ruclem13  13825  ramtub  14378  elbasfv  14526  elbasov  14527  restsspw  14676  homarcl  15202  grpidval  15738  odlem2  16352  efgrelexlema  16556  subcmn  16631  dvdsrval  17071  pf1rcl  18149  elocv  18459  matrcl  18674  0top  19244  ppttop  19267  pptbas  19268  restrcl  19417  ssrest  19436  iscnp2  19499  lmmo  19640  zfbas  20125  rnelfmlem  20181  isfcls  20238  isnghm  20958  iscau2  21444  itg2cnlem1  21896  itgsubstlem  22177  dchrrcl  23236  eleenn  23868  nbgranself2  24098  uvtxisvtx  24152  uvtx01vtx  24154  2spot0  24727  hon0  26374  dmadjrnb  26487  eulerpartlemgvv  27941  indispcon  28305  cvmtop1  28331  cvmtop2  28332  funpartlem  29155  tailfb  29785  mapco2g  30237  wepwsolem  30580  ssfiunibd  31041  bnj98  32879  atbase  33961  llnbase  34180  lplnbase  34205  lvolbase  34249  osumcllem4N  34630  pexmidlem1N  34641  lhpbase  34669