Theorem ne0i 3752

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

Assertion

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

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3751	. 2 |- ( B e. A -> -. A = (/) )
2	1	neneqad 2656	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1758   =/= wne 2648   (/)c0 3746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3440  df-nul 3747

This theorem is referenced by:  vn0  3753  inelcm  3842  rzal  3890  rexn0  3891  snnzg  4101  prnz  4103  tpnz  4105  tpnzd  4106  brne0  4448  exss  4664  ord0eln0  4882  onn0  4892  elfvdm  5826  isofrlem  6141  fr3nr  6502  onnmin  6525  f1oweALT  6672  bropopvvv  6764  frxp  6793  mpt2xopxnop0  6843  brovex  6851  fvmpt2curryd  6901  onnseq  6916  oe1m  7095  oawordeulem  7104  oa00  7109  oarec  7112  omord  7118  oewordri  7142  oeordsuc  7144  oelim2  7145  oeoalem  7146  oeoelem  7148  oeeui  7152  nnmord  7182  nnawordex  7187  map0g  7363  ixpn0  7406  omxpenlem  7523  frfi  7669  unblem1  7676  wofib  7871  canthwdom  7906  inf1  7940  noinfep  7977  noinfepOLD  7978  oemapvali  8004  cantnflem1a  8005  cantnflem1d  8008  cantnflem1  8009  cantnf  8013  cantnflem1aOLD  8028  cantnflem1dOLD  8031  cantnflem1OLD  8032  cantnfOLD  8035  epfrs  8063  acnrcl  8324  iunfictbso  8396  dfac5lem2  8406  dfac9  8417  kmlem6  8436  fin23lem31  8624  fin23lem40  8632  isf34lem7  8660  isf34lem6  8661  isfin1-3  8667  fin1a2lem7  8687  fin1a2lem13  8693  axdc3lem4  8734  alephval2  8848  omina  8970  intwun  9014  r1limwun  9015  tskpr  9049  inar1  9054  tskuni  9062  tskxp  9066  tskmap  9067  gruina  9097  grur1a  9098  grur1  9099  axgroth3  9110  inaprc  9115  addclpi  9173  mulclpi  9174  indpi  9188  nqerf  9211  genpn0  9284  supsrlem  9390  axpre-sup  9448  infmrcl  10421  infmrlb  10423  uzn0  10988  infmssuzle  11049  suprzub  11058  rpnnen1lem4  11094  rpnnen1lem5  11095  eliooxr  11466  iccssioo2  11480  iccsupr  11500  fzn0  11582  elfzoel1  11669  elfzoel2  11670  fzon0  11687  flval3  11781  icopnfsup  11822  fseqsupubi  11918  hashnn0n0nn  12272  sqrlem3  12853  rexfiuz  12954  r19.2uz  12958  climuni  13149  isercolllem2  13262  isercolllem3  13263  climsup  13266  caurcvg  13273  caurcvg2  13274  caucvg  13275  infcvgaux1i  13438  mertenslem2  13464  ruclem11  13641  divalglem2  13718  gcdcllem1  13814  bezoutlem2  13842  pclem  14024  pc2dvds  14064  prmreclem1  14096  prmreclem6  14101  4sqlem13  14137  vdwmc2  14159  vdwlem6  14166  vdwlem8  14168  vdwnnlem3  14177  ramtcl  14190  mrcflem  14664  mrcval  14668  iscatd2  14739  fpwipodrs  15454  gsumval2  15633  grpbn0  15687  issubgrpd2  15817  issubg3  15819  issubg4  15820  subgint  15825  cycsubgcl  15827  nmzsubg  15842  ghmpreima  15888  brgici  15918  gastacl  15947  odlem2  16164  gexlem2  16203  sylow1lem5  16223  pgpssslw  16235  sylow2alem2  16239  sylow2blem3  16243  fislw  16246  sylow3lem3  16250  sylow3lem4  16251  torsubg  16458  oddvdssubg  16459  iscygd  16486  iscygodd  16487  cyggexb  16497  gsumval3OLD  16504  gsumval3  16507  dprdsubg  16644  ablfacrp2  16691  ablfac1c  16695  ablfac1eu  16697  pgpfaclem2  16706  subrgugrp  17008  cntzsubr  17021  islss4  17167  lss1d  17168  lssintcl  17169  brlmici  17274  lspsolvlem  17347  lbsextlem1  17363  lidlsubg  17421  abvn0b  17498  psrbas  17572  psrbasOLD  17573  mplsubglem  17635  mpllsslem  17636  mplsubglemOLD  17637  mpllsslemOLD  17638  ltbwe  17679  mplind  17709  mpfrcl  17729  ply1plusgfvi  17821  ply1frcl  17879  cnsubglem  17988  cnmsubglem  18001  zringlpirlem1  18029  zlpirlem1  18034  ocvlss  18223  lmiclbs  18392  lmisfree  18397  cramerimplem2  18623  cramerimplem3  18624  cramerimp  18625  clscld  18784  clsval2  18787  lmmo  19117  1stcfb  19182  2ndcdisj  19193  2ndcsep  19196  ptclsg  19321  dfac14lem  19323  txindis  19340  hmphi  19483  opnfbas  19548  trfbas2  19549  isfil2  19562  filn0  19568  zfbas  19602  filssufilg  19617  rnelfmlem  19658  flimclslem  19690  flimfnfcls  19734  ptcmplem2  19758  clssubg  19812  tgpconcomp  19816  tsmsfbas  19831  ustfilxp  19920  ustne0  19921  prdsmet  20078  xbln0  20122  bln0  20123  prdsbl  20199  metustfbasOLD  20273  metustfbas  20274  metustblOLD  20288  metustbl  20289  nrgdomn  20385  nrginvrcn  20405  tgioo  20506  icccmplem2  20533  icccmplem3  20534  reconnlem2  20537  lebnumlem3  20668  phtpcer  20700  reparpht  20703  phtpcco2  20704  pcohtpy  20725  pcorevlem  20731  caun0  20925  iscmet3lem2  20936  bcthlem4  20971  cnflduss  21001  cnfldcusp  21002  reust  21018  recusp  21019  minveclem3b  21048  ivthlem2  21069  ivthlem3  21070  evthicc  21076  ovollb2  21105  ovolctb  21106  ovolunlem1a  21112  ovolunlem1  21113  ovoliunlem1  21118  ovoliun2  21122  nulmbl2  21152  ioombl1lem4  21176  uniioombllem1  21195  uniioombllem2  21197  uniioombllem6  21202  mbfsup  21276  mbfinf  21277  mbflimsup  21278  itg1climres  21326  itg2seq  21354  itg2monolem1  21362  itg2mono  21365  itg2i1fseq2  21368  dvferm1lem  21590  dvferm2lem  21592  dvferm  21594  c1liplem1  21602  c1lip1  21603  dvivthlem1  21614  aannenlem2  21929  aalioulem2  21933  ulm0  21990  pilem2  22051  pilem3  22052  birthdaylem1  22479  ftalem3  22546  ftalem4  22547  ftalem5  22548  dchrabs  22733  pntlem3  22992  tgldimor  23091  axlowdimlem13  23353  axlowdim1  23358  ghgrp  24008  nvo00  24314  nmorepnf  24321  ubthlem1  24424  minvecolem1  24428  shintcl  24886  chintcl  24888  nmoprepnf  25424  nmfnrepnf  25437  nmcexi  25583  snct  26163  submomnd  26319  slmdbn0  26370  slmdsn0  26373  suborng  26429  ordtconlem1  26500  rge0scvg  26525  qqhucn  26567  rrhre  26593  esum0  26649  esumpcvgval  26673  sigagenval  26729  voliune  26790  oddpwdc  26882  eulerpartlemt  26899  erdszelem2  27225  erdszelem8  27231  txsconlem  27274  cvxscon  27277  cvmsss2  27308  cvmliftmolem2  27316  cvmlift2lem12  27348  cvmliftpht  27352  dfrtrcl2  27495  dfso3  27521  sltval2  27942  nocvxminlem  27976  nobndlem5  27982  onint1  28440  heicant  28575  mblfinlem2  28578  ismblfin  28581  ovoliunnfl  28582  voliunnfl  28584  volsupnfl  28585  itg2addnclem  28592  itg2addnc  28595  ftc1anclem7  28622  ftc1anc  28624  finminlem  28662  fnemeet1  28736  fnejoin1  28738  tailfb  28747  incsequz  28793  isbnd3  28832  ssbnd  28836  totbndbnd  28837  prdsbnd  28841  prdsbnd2  28843  heibor1lem  28857  prtlem100  29149  prter3  29176  nacsfix  29197  mzpcln0  29213  rencldnfilem  29308  rencldnfi  29309  fnwe2lem2  29553  kelac1  29565  harn0  29607  hbtlem2  29629  rzalf  29888  ubelsupr  29891  climinf  29928  stoweidlem11  29955  stoweidlem31  29975  stoweidlem34  29978  stoweidlem36  29980  stoweidlem59  30003  stirlinglem13  30030  2reu4  30163  elfvmptrab1  30303  elovmpt3imp  30309  2wlkonot3v  30543  2spthonot3v  30544  usg2spthonot  30556  usg2spthonot0  30557  2spot2iun2spont  30559  clwwlknprop  30584  frg2wotn0  30798  supgtoreq  30892  supfirege  30893  01eq0rng  30926  dmatsgrp  31058  scmatsgrp  31065  scmatsgrp1  31069  lincolss  31101  abln0  31157  rngn0  31161  lmodn0  31170  cpmatsubgpmat  31210  pmatcollpw3  31272  bnj906  32256  bnj1177  32330  bnj1523  32395  bj-tagn0  32805  lkrlss  33079  ishlat3N  33338  hlsupr2  33370  elpaddri  33785  pclvalN  33873  dian0  35023  diaintclN  35042  docaclN  35108  dibintclN  35151  dicn0  35176  dihglblem5  35282  dihglb2  35326  dihintcl  35328  doch2val2  35348  dochocss  35350  lclkr  35517  lclkrs  35523  lcfr  35569  taupi  35956