Theorem n0i 3735

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 3734	. . 3 |- -. B e. (/)
2		eleq2 2517	. . 3 |- ( A = (/) -> ( B e. A <-> B e. (/) ) )
3	1, 2	mtbiri 305	. 2 |- ( A = (/) -> -. B e. A )
4	3	con2i 124	1 |- ( B e. A -> -. A = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1443   e. wcel 1886   (/)c0 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-dif 3406  df-nul 3731

This theorem is referenced by:  ne0i  3736  oprcl  4190  disjss3  4400  iin0  4576  snsn0non  5540  mptrcl  5953  isomin  6226  ovrcl  6321  tfrlem16  7108  oalimcl  7258  omlimcl  7276  oaabs2  7343  ecexr  7365  elpmi  7487  elmapex  7489  pmresg  7496  pmsspw  7503  ixpssmap2g  7548  ixpssmapg  7549  resixpfo  7557  php3  7755  cantnfp1lem2  8181  cantnflem1  8191  cnfcom2lem  8203  rankxplim2  8348  rankxplim3  8349  cardlim  8403  alephnbtwn  8499  pwcdadom  8643  ttukeylem5  8940  r1wunlim  9159  nnunb  10862  ssnn0fi  12194  ruclem13  14287  ramtub  14961  ramtubOLD  14962  elbasfv  15163  elbasov  15164  restsspw  15323  homarcl  15916  grpidval  16496  odlem2  17181  odlem2OLD  17197  efgrelexlema  17392  subcmn  17470  dvdsrval  17866  pf1rcl  18930  elocv  19224  matrcl  19430  0top  19992  ppttop  20015  pptbas  20016  restrcl  20166  ssrest  20185  iscnp2  20248  lmmo  20389  zfbas  20904  rnelfmlem  20960  isfcls  21017  isnghm  21721  isnghmOLD  21739  iscau2  22240  itg2cnlem1  22712  itgsubstlem  22993  dchrrcl  24161  eleenn  24919  nbgranself2  25157  uvtxisvtx  25211  uvtx01vtx  25213  2spot0  25785  hon0  27439  dmadjrnb  27552  eulerpartlemgvv  29202  bnj98  29671  indispcon  29950  cvmtop1  29976  cvmtop2  29977  mrsub0  30147  mrsubf  30148  mrsubccat  30149  mrsubcn  30150  mrsubco  30152  mrsubvrs  30153  msubf  30163  mclsrcl  30192  funpartlem  30702  tailfb  31026  atbase  32849  llnbase  33068  lplnbase  33093  lvolbase  33137  osumcllem4N  33518  pexmidlem1N  33529  lhpbase  33557  mapco2g  35550  wepwsolem  35894  ssfiunibd  37521  hoicvr  38364