Theorem n0i 3593

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 3592	. . 3 |- -. B e. (/)
2		eleq2 2465	. . 3 |- ( A = (/) -> ( B e. A <-> B e. (/) ) )
3	1, 2	mtbiri 295	. 2 |- ( A = (/) -> -. B e. A )
4	3	con2i 114	1 |- ( B e. A -> -. A = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1649   e. wcel 1721   (/)c0 3588

This theorem is referenced by:  ne0i  3594  oprcl  3968  disjss3  4171  iin0  4333  snsn0non  4659  isomin  6016  ovrcl  6070  tfrlem16  6613  oalimcl  6762  omlimcl  6780  oaabs2  6847  ecexr  6869  elpmi  6994  elmapex  6996  pmresg  7000  pmsspw  7007  ixpssmap2g  7050  ixpssmapg  7051  resixpfo  7059  php3  7252  cantnfp1lem2  7591  cantnflem1  7601  cnfcom2lem  7614  rankxplim2  7760  rankxplim3  7761  cardlim  7815  alephnbtwn  7908  pwcdadom  8052  ttukeylem5  8349  r1wunlim  8568  nnunb  10173  ruclem13  12796  ramtub  13335  elbasfv  13467  elbasov  13468  restsspw  13614  homarcl  14138  grpidval  14662  odlem2  15132  efgrelexlema  15336  subcmn  15411  dvdsrval  15705  elocv  16850  0top  17003  ppttop  17026  pptbas  17027  restrcl  17175  ssrest  17194  iscnp2  17257  lmmo  17398  zfbas  17881  rnelfmlem  17937  isfcls  17994  isnghm  18710  iscau2  19183  itg2cnlem1  19606  itgsubstlem  19885  pf1rcl  19922  dchrrcl  20977  nbgranself2  21401  uvtxisvtx  21452  uvtx01vtx  21454  hon0  23249  dmadjrnb  23362  indispcon  24874  cvmtop1  24900  cvmtop2  24901  funpartlem  25695  eleenn  25739  tailfb  26296  mapco2g  26659  wepwsolem  27006  matrcl  27334  2spot0  28167  bnj98  28944  atbase  29772  llnbase  29991  lplnbase  30016  lvolbase  30060  osumcllem4N  30441  pexmidlem1N  30452  lhpbase  30480

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-nul 3589