Theorem n0i 3645

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 3644	. . 3 |- -. B e. (/)
2		eleq2 2504	. . 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 1369   e. wcel 1756   (/)c0 3640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-dif 3334  df-nul 3641

This theorem is referenced by:  ne0i  3646  oprcl  4087  disjss3  4294  iin0  4469  snsn0non  4840  isomin  6031  ovrcl  6124  tfrlem16  6855  oalimcl  7002  omlimcl  7020  oaabs2  7087  ecexr  7109  elpmi  7234  elmapex  7236  pmresg  7243  pmsspw  7250  ixpssmap2g  7295  ixpssmapg  7296  resixpfo  7304  php3  7500  cantnfp1lem2  7890  cantnflem1  7900  cantnfp1lem2OLD  7916  cantnflem1OLD  7923  cnfcom2lem  7937  cnfcom2lemOLD  7945  rankxplim2  8090  rankxplim3  8091  cardlim  8145  alephnbtwn  8244  pwcdadom  8388  ttukeylem5  8685  r1wunlim  8907  nnunb  10578  ruclem13  13527  ramtub  14076  elbasfv  14224  elbasov  14225  restsspw  14373  homarcl  14899  grpidval  15435  odlem2  16045  efgrelexlema  16249  subcmn  16324  dvdsrval  16740  pf1rcl  17786  elocv  18096  matrcl  18315  0top  18591  ppttop  18614  pptbas  18615  restrcl  18764  ssrest  18783  iscnp2  18846  lmmo  18987  zfbas  19472  rnelfmlem  19528  isfcls  19585  isnghm  20305  iscau2  20791  itg2cnlem1  21242  itgsubstlem  21523  dchrrcl  22582  eleenn  23145  nbgranself2  23350  uvtxisvtx  23401  uvtx01vtx  23403  hon0  25200  dmadjrnb  25313  eulerpartlemgvv  26762  indispcon  27126  cvmtop1  27152  cvmtop2  27153  funpartlem  27976  tailfb  28601  mapco2g  29053  wepwsolem  29397  2spot0  30660  ssnn0fi  30749  bnj98  31863  atbase  32937  llnbase  33156  lplnbase  33181  lvolbase  33225  osumcllem4N  33606  pexmidlem1N  33617  lhpbase  33645