Theorem ne0i 3638

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 3637	. 2 |- ( B e. A -> -. A = (/) )
2	1	neneqad 2676	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1756   =/= wne 2601   (/)c0 3632

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 2419

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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-nul 3633

This theorem is referenced by:  vn0  3639  inelcm  3728  rzal  3776  rexn0  3777  snnzg  3987  prnz  3989  tpnz  3991  tpnzd  3992  brne0  4334  exss  4550  ord0eln0  4768  onn0  4778  elfvdm  5711  isofrlem  6026  fr3nr  6386  onnmin  6409  f1oweALT  6556  bropopvvv  6648  frxp  6677  mpt2xopxnop0  6727  brovex  6735  onnseq  6797  oe1m  6976  oawordeulem  6985  oa00  6990  oarec  6993  omord  6999  oewordri  7023  oeordsuc  7025  oelim2  7026  oeoalem  7027  oeoelem  7029  oeeui  7033  nnmord  7063  nnawordex  7068  map0g  7244  ixpn0  7287  omxpenlem  7404  frfi  7549  unblem1  7556  wofib  7751  canthwdom  7786  inf1  7820  noinfep  7857  noinfepOLD  7858  oemapvali  7884  cantnflem1a  7885  cantnflem1d  7888  cantnflem1  7889  cantnf  7893  cantnflem1aOLD  7908  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnfOLD  7915  epfrs  7943  acnrcl  8204  iunfictbso  8276  dfac5lem2  8286  dfac9  8297  kmlem6  8316  fin23lem31  8504  fin23lem40  8512  isf34lem7  8540  isf34lem6  8541  isfin1-3  8547  fin1a2lem7  8567  fin1a2lem13  8573  axdc3lem4  8614  alephval2  8728  omina  8850  intwun  8894  r1limwun  8895  tskpr  8929  inar1  8934  tskuni  8942  tskxp  8946  tskmap  8947  gruina  8977  grur1a  8978  grur1  8979  axgroth3  8990  inaprc  8995  addclpi  9053  mulclpi  9054  indpi  9068  nqerf  9091  genpn0  9164  supsrlem  9270  axpre-sup  9328  infmrcl  10301  infmrlb  10303  uzn0  10868  infmssuzle  10929  suprzub  10938  rpnnen1lem4  10974  rpnnen1lem5  10975  eliooxr  11346  iccssioo2  11360  iccsupr  11374  fzn0  11456  elfzoel1  11543  elfzoel2  11544  fzon0  11561  flval3  11655  icopnfsup  11696  fseqsupubi  11792  hashnn0n0nn  12145  sqrlem3  12726  rexfiuz  12827  r19.2uz  12831  climuni  13022  isercolllem2  13135  isercolllem3  13136  climsup  13139  caurcvg  13146  caurcvg2  13147  caucvg  13148  infcvgaux1i  13311  mertenslem2  13337  ruclem11  13514  divalglem2  13591  gcdcllem1  13687  bezoutlem2  13715  pclem  13897  pc2dvds  13937  prmreclem1  13969  prmreclem6  13974  4sqlem13  14010  vdwmc2  14032  vdwlem6  14039  vdwlem8  14041  vdwnnlem3  14050  ramtcl  14063  mrcflem  14536  mrcval  14540  iscatd2  14611  fpwipodrs  15326  gsumval2  15504  grpbn0  15558  issubgrpd2  15688  issubg3  15690  issubg4  15691  subgint  15696  cycsubgcl  15698  nmzsubg  15713  ghmpreima  15759  brgici  15789  gastacl  15818  odlem2  16033  gexlem2  16072  sylow1lem5  16092  pgpssslw  16104  sylow2alem2  16108  sylow2blem3  16112  fislw  16115  sylow3lem3  16119  sylow3lem4  16120  torsubg  16327  oddvdssubg  16328  iscygd  16355  iscygodd  16356  cyggexb  16366  gsumval3OLD  16373  gsumval3  16376  dprdsubg  16509  ablfacrp2  16556  ablfac1c  16560  ablfac1eu  16562  pgpfaclem2  16571  subrgugrp  16862  cntzsubr  16875  islss4  17020  lss1d  17021  lssintcl  17022  brlmici  17127  lspsolvlem  17200  lbsextlem1  17216  lidlsubg  17274  abvn0b  17351  psrbas  17425  psrbasOLD  17426  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  ltbwe  17529  mplind  17559  mpfrcl  17579  ply1plusgfvi  17672  ply1frcl  17728  cnsubglem  17837  cnmsubglem  17850  zringlpirlem1  17878  zlpirlem1  17883  ocvlss  18072  lmiclbs  18241  lmisfree  18246  cramerimplem2  18465  cramerimplem3  18466  cramerimp  18467  clscld  18626  clsval2  18629  lmmo  18959  1stcfb  19024  2ndcdisj  19035  2ndcsep  19038  ptclsg  19163  dfac14lem  19165  txindis  19182  hmphi  19325  opnfbas  19390  trfbas2  19391  isfil2  19404  filn0  19410  zfbas  19444  filssufilg  19459  rnelfmlem  19500  flimclslem  19532  flimfnfcls  19576  ptcmplem2  19600  clssubg  19654  tgpconcomp  19658  tsmsfbas  19673  ustfilxp  19762  ustne0  19763  prdsmet  19920  xbln0  19964  bln0  19965  prdsbl  20041  metustfbasOLD  20115  metustfbas  20116  metustblOLD  20130  metustbl  20131  nrgdomn  20227  nrginvrcn  20247  tgioo  20348  icccmplem2  20375  icccmplem3  20376  reconnlem2  20379  lebnumlem3  20510  phtpcer  20542  reparpht  20545  phtpcco2  20546  pcohtpy  20567  pcorevlem  20573  caun0  20767  iscmet3lem2  20778  bcthlem4  20813  cnflduss  20843  cnfldcusp  20844  reust  20860  recusp  20861  minveclem3b  20890  ivthlem2  20911  ivthlem3  20912  evthicc  20918  ovollb2  20947  ovolctb  20948  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliun2  20964  nulmbl2  20993  ioombl1lem4  21017  uniioombllem1  21036  uniioombllem2  21038  uniioombllem6  21043  mbfsup  21117  mbfinf  21118  mbflimsup  21119  itg1climres  21167  itg2seq  21195  itg2monolem1  21203  itg2mono  21206  itg2i1fseq2  21209  dvferm1lem  21431  dvferm2lem  21433  dvferm  21435  c1liplem1  21443  c1lip1  21444  dvivthlem1  21455  aannenlem2  21770  aalioulem2  21774  ulm0  21831  pilem2  21892  pilem3  21893  birthdaylem1  22320  ftalem3  22387  ftalem4  22388  ftalem5  22389  dchrabs  22574  pntlem3  22833  tgldimor  22930  axlowdimlem13  23151  axlowdim1  23156  ghgrp  23806  nvo00  24112  nmorepnf  24119  ubthlem1  24222  minvecolem1  24226  shintcl  24684  chintcl  24686  nmoprepnf  25222  nmfnrepnf  25235  nmcexi  25381  snct  25962  submomnd  26124  slmdbn0  26175  slmdsn0  26178  suborng  26234  ordtconlem1  26306  rge0scvg  26331  qqhucn  26373  rrhre  26399  esum0  26455  esumpcvgval  26479  sigagenval  26535  voliune  26597  oddpwdc  26689  eulerpartlemt  26706  erdszelem2  27032  erdszelem8  27038  txsconlem  27081  cvxscon  27084  cvmsss2  27115  cvmliftmolem2  27123  cvmlift2lem12  27155  cvmliftpht  27159  dfrtrcl2  27301  dfso3  27327  sltval2  27748  nocvxminlem  27782  nobndlem5  27788  onint1  28247  heicant  28379  mblfinlem2  28382  ismblfin  28385  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  itg2addnclem  28396  itg2addnc  28399  ftc1anclem7  28426  ftc1anc  28428  finminlem  28466  fnemeet1  28540  fnejoin1  28542  tailfb  28551  incsequz  28597  isbnd3  28636  ssbnd  28640  totbndbnd  28641  prdsbnd  28645  prdsbnd2  28647  heibor1lem  28661  prtlem100  28953  prter3  28980  nacsfix  29001  mzpcln0  29017  rencldnfilem  29112  rencldnfi  29113  fnwe2lem2  29357  kelac1  29369  harn0  29411  hbtlem2  29433  rzalf  29692  ubelsupr  29695  climinf  29732  stoweidlem11  29759  stoweidlem31  29779  stoweidlem34  29782  stoweidlem36  29784  stoweidlem59  29807  stirlinglem13  29834  2reu4  29967  elfvmptrab1  30107  elovmpt3imp  30113  2wlkonot3v  30347  2spthonot3v  30348  usg2spthonot  30360  usg2spthonot0  30361  2spot2iun2spont  30363  clwwlknprop  30388  frg2wotn0  30602  supgtoreq  30694  supfirege  30695  01eq0rng  30728  dmatsgrp  30801  scmatsgrp  30808  scmatsgrp1  30812  lincolss  30857  abln0  30913  rngn0  30917  lmodn0  30926  bnj906  31810  bnj1177  31884  bnj1523  31949  bj-tagn0  32319  lkrlss  32580  ishlat3N  32839  hlsupr2  32871  elpaddri  33286  pclvalN  33374  dian0  34524  diaintclN  34543  docaclN  34609  dibintclN  34652  dicn0  34677  dihglblem5  34783  dihglb2  34827  dihintcl  34829  doch2val2  34849  dochocss  34851  lclkr  35018  lclkrs  35024  lcfr  35070  taupi  35457