Theorem ne0i 3789

Description: If a set has elements, then 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 3788	. 2 |- ( B e. A -> -. A = (/) )
2	1	neqned 2657	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1823   =/= wne 2649   (/)c0 3783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-nul 3784

This theorem is referenced by:  ne0ii  3790  inelcm  3869  rzal  3919  rexn0  3920  snnzg  4133  tpnzd  4138  brne0  4486  exss  4700  ord0eln0  4921  elfvdm  5874  elfvmptrab1  5952  isofrlem  6211  elovmpt3imp  6506  onnmin  6611  f1oweALT  6757  bropopvvv  6853  frxp  6883  mpt2xopxnop0  6935  brovex  6942  fvmpt2curryd  6992  onnseq  7007  oe1m  7186  oa00  7200  oarec  7203  omord  7209  oewordri  7233  oeordsuc  7235  oelim2  7236  oeoalem  7237  oeoelem  7239  oeeui  7243  nnmord  7273  nnawordex  7278  map0g  7451  ixpn0  7494  omxpenlem  7611  frfi  7757  unblem1  7764  supgtoreq  7920  wofib  7962  canthwdom  7997  inf1  8030  noinfepOLD  8068  oemapvali  8094  cantnflem1a  8095  cantnflem1d  8098  cantnflem1  8099  cantnf  8103  cantnflem1aOLD  8118  cantnflem1dOLD  8121  cantnflem1OLD  8122  cantnfOLD  8125  epfrs  8153  acnrcl  8414  iunfictbso  8486  dfac5lem2  8496  dfac9  8507  kmlem6  8526  fin23lem40  8722  isf34lem7  8750  isf34lem6  8751  fin1a2lem7  8777  fin1a2lem13  8783  axdc3lem4  8824  alephval2  8938  intwun  9102  r1limwun  9103  tskpr  9137  inar1  9142  tskuni  9150  tskxp  9154  tskmap  9155  gruina  9185  grur1a  9186  grur1  9187  axgroth3  9198  inaprc  9203  addclpi  9259  mulclpi  9260  indpi  9274  nqerf  9297  genpn0  9370  supsrlem  9477  axpre-sup  9535  infmrcl  10517  infmrlb  10519  supfirege  10520  uzn0  11097  infmssuzle  11165  suprzub  11174  eliooxr  11586  iccssioo2  11600  iccsupr  11620  fzn0  11703  elfzoel1  11802  elfzoel2  11803  fzon0  11821  flval3  11932  icopnfsup  11974  fseqsupubi  12073  hashnn0n0nn  12445  swrdn0  12649  dfrtrcl2  12980  sqrlem3  13163  r19.2uz  13269  climuni  13460  isercolllem2  13573  isercolllem3  13574  climsup  13577  mertenslem2  13779  ruclem11  14060  gcdcllem1  14236  bezoutlem2  14264  pclem  14449  prmreclem1  14521  prmreclem6  14526  4sqlem13  14562  vdwmc2  14584  vdwlem6  14591  vdwlem8  14593  vdwnnlem3  14602  ramtcl  14615  mrcflem  15098  mrcval  15102  iscatd2  15173  fpwipodrs  15996  gsumval2  16109  mgm2nsgrplem1  16238  sgrp2nmndlem1  16243  grpbn0  16281  issubgrpd2  16419  issubg3  16421  issubg4  16422  subgint  16427  cycsubgcl  16429  nmzsubg  16444  ghmpreima  16490  brgici  16520  gastacl  16549  odlem2  16765  gexlem2  16804  sylow1lem5  16824  pgpssslw  16836  sylow2alem2  16840  sylow2blem3  16844  fislw  16847  sylow3lem3  16851  sylow3lem4  16852  torsubg  17062  oddvdssubg  17063  abln0  17075  iscygd  17092  iscygodd  17093  cyggexb  17103  gsumval3OLD  17110  gsumval3  17113  dprdsubg  17269  ablfacrp2  17316  ablfac1c  17320  ablfac1eu  17322  pgpfaclem2  17331  ringn0  17447  subrgugrp  17646  cntzsubr  17659  islss4  17806  lss1d  17807  lssintcl  17808  brlmici  17913  lspsolvlem  17986  lbsextlem1  18002  lidlsubg  18060  01eq0ring  18118  abvn0b  18149  psrbas  18228  psrbasOLD  18229  mplsubglem  18291  mpllsslem  18292  mplsubglemOLD  18293  mpllsslemOLD  18294  ltbwe  18335  mplind  18365  mpfrcl  18385  ply1plusgfvi  18481  ply1frcl  18553  zringlpirlem1  18700  ocvlss  18879  lmiclbs  19042  lmisfree  19047  mat1ric  19159  dmatsgrp  19171  scmatsgrp  19191  scmatsgrp1  19194  scmatlss  19197  scmatric  19209  cramerimplem2  19356  cramerimplem3  19357  cramerimp  19358  cpmatsubgpmat  19391  matcpmric  19430  pmmpric  19494  clscld  19718  clsval2  19721  lmmo  20051  1stcfb  20115  2ndcdisj  20126  2ndcsep  20129  ptclsg  20285  dfac14lem  20287  txindis  20304  hmphi  20447  opnfbas  20512  trfbas2  20513  isfil2  20526  filn0  20532  filssufilg  20581  rnelfmlem  20622  flimclslem  20654  flimfnfcls  20698  ptcmplem2  20722  clssubg  20776  tgpconcomp  20780  tsmsfbas  20795  ustfilxp  20884  ustne0  20885  prdsmet  21042  xbln0  21086  bln0  21087  prdsbl  21163  metustfbasOLD  21237  metustfbas  21238  metustblOLD  21252  metustbl  21253  nrgdomn  21349  tgioo  21470  icccmplem2  21497  icccmplem3  21498  reconnlem2  21501  phtpcer  21664  reparpht  21667  phtpcco2  21668  pcohtpy  21689  pcorevlem  21695  caun0  21889  iscmet3lem2  21900  bcthlem4  21935  minveclem3b  22012  ivthlem2  22033  ivthlem3  22034  evthicc  22040  ovollb2  22069  ovolctb  22070  ovolunlem1a  22076  ovolunlem1  22077  ovoliunlem1  22082  ovoliun2  22086  ioombl1lem4  22140  uniioombllem1  22159  uniioombllem2  22161  uniioombllem6  22166  mbfsup  22240  mbfinf  22241  mbflimsup  22242  itg1climres  22290  itg2monolem1  22326  itg2mono  22329  itg2i1fseq2  22332  dvferm1lem  22554  dvferm2lem  22556  dvferm  22558  c1liplem1  22566  dvivthlem1  22578  aalioulem2  22898  ulm0  22955  pilem2  23016  pilem3  23017  birthdaylem1  23482  ftalem3  23549  ftalem4  23550  ftalem5  23551  dchrabs  23736  pntlem3  23995  tgldimor  24097  tglnne0  24224  axlowdimlem13  24462  axlowdim1  24467  clwwlknprop  24977  2wlkonot3v  25080  2spthonot3v  25081  usg2spthonot  25093  usg2spthonot0  25094  2spot2iun2spont  25096  frg2wotn0  25261  ghgrpOLD  25571  nvo00  25877  nmorepnf  25884  ubthlem1  25987  minvecolem1  25991  submomnd  27937  slmdbn0  27988  slmdsn0  27991  suborng  28043  ordtconlem1  28144  rge0scvg  28169  qqhucn  28210  rrhre  28236  sigagenval  28373  voliune  28441  oddpwdc  28560  eulerpartlemt  28577  erdszelem2  28903  erdszelem8  28909  txsconlem  28952  cvxscon  28955  cvmsss2  28986  cvmliftmolem2  28994  cvmlift2lem12  29026  cvmliftpht  29030  dfso3  29341  sltval2  29659  nocvxminlem  29693  nobndlem5  29699  onint1  30145  heicant  30292  mblfinlem2  30295  ismblfin  30298  ovoliunnfl  30299  voliunnfl  30301  itg2addnc  30312  ftc1anclem7  30339  ftc1anc  30341  finminlem  30379  fnemeet1  30427  fnejoin1  30429  tailfb  30438  totbndbnd  30528  prdsbnd  30532  prdsbnd2  30534  heibor1lem  30548  prtlem100  30839  prter3  30866  nacsfix  30887  mzpcln0  30903  rencldnfilem  30996  rencldnfi  30997  fnwe2lem2  31239  kelac1  31251  harn0  31295  hbtlem2  31317  prmunb2  31435  lcmgcdlem  31456  rzalf  31635  ubelsupr  31638  suprnmpt  31694  ssfiunibd  31751  climinf  31854  limclr  31903  jumpncnp  31943  ioodvbdlimc1lem1  31970  ioodvbdlimc1lem2  31971  ioodvbdlimc1  31972  ioodvbdlimc2lem  31973  ioodvbdlimc2  31974  stoweidlem11  32035  stoweidlem31  32055  stoweidlem34  32058  stoweidlem36  32060  stoweidlem59  32083  fourierdlem20  32151  fourierdlem25  32156  fourierdlem31  32162  fourierdlem37  32168  fourierdlem42  32173  fourierdlem46  32177  fourierdlem48  32179  fourierdlem49  32180  fourierdlem52  32183  fourierdlem54  32185  fourierdlem64  32195  fourierdlem73  32204  fourierdlem79  32210  fouriercn  32257  elaa2lem  32258  2reu4  32437  cznrng  33036  lincolss  33308  lmodn0  33369  aacllem  33623  bnj1177  34482  bnj1523  34547  lkrlss  35236  ishlat3N  35495  hlsupr2  35527  elpaddri  35942  pclvalN  36030  dian0  37182  diaintclN  37201  docaclN  37267  dibintclN  37310  dicn0  37335  dihglblem5  37441  dihglb2  37485  dihintcl  37487  doch2val2  37507  dochocss  37509  lclkr  37676  lclkrs  37682  lcfr  37728