Theorem ne0i 3631

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

Syntax hints:   -> wi 4   e. wcel 1755   =/= wne 2596   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  vn0  3632  inelcm  3721  rzal  3769  rexn0  3770  snnzg  3980  prnz  3982  tpnz  3984  tpnzd  3985  brne0  4327  exss  4543  ord0eln0  4760  onn0  4770  elfvdm  5704  isofrlem  6018  fr3nr  6380  onnmin  6403  f1oweALT  6550  bropopvvv  6642  frxp  6671  mpt2xopxnop0  6721  brovex  6729  onnseq  6791  oe1m  6972  oawordeulem  6981  oa00  6986  oarec  6989  omord  6995  oewordri  7019  oeordsuc  7021  oelim2  7022  oeoalem  7023  oeoelem  7025  oeeui  7029  nnmord  7059  nnawordex  7064  map0g  7240  ixpn0  7283  omxpenlem  7400  frfi  7545  unblem1  7552  wofib  7747  canthwdom  7782  inf1  7816  noinfep  7853  noinfepOLD  7854  oemapvali  7880  cantnflem1a  7881  cantnflem1d  7884  cantnflem1  7885  cantnf  7889  cantnflem1aOLD  7904  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnfOLD  7911  epfrs  7939  acnrcl  8200  iunfictbso  8272  dfac5lem2  8282  dfac9  8293  kmlem6  8312  fin23lem31  8500  fin23lem40  8508  isf34lem7  8536  isf34lem6  8537  isfin1-3  8543  fin1a2lem7  8563  fin1a2lem13  8569  axdc3lem4  8610  alephval2  8724  omina  8846  intwun  8890  r1limwun  8891  tskpr  8925  inar1  8930  tskuni  8938  tskxp  8942  tskmap  8943  gruina  8973  grur1a  8974  grur1  8975  axgroth3  8986  inaprc  8991  addclpi  9049  mulclpi  9050  indpi  9064  nqerf  9087  genpn0  9160  supsrlem  9266  axpre-sup  9324  infmrcl  10297  infmrlb  10299  uzn0  10864  infmssuzle  10925  suprzub  10934  rpnnen1lem4  10970  rpnnen1lem5  10971  eliooxr  11342  iccssioo2  11356  iccsupr  11370  fzn0  11451  elfzoel1  11535  elfzoel2  11536  fzon0  11553  flval3  11647  icopnfsup  11688  fseqsupubi  11784  hashnn0n0nn  12137  sqrlem3  12718  rexfiuz  12819  r19.2uz  12823  climuni  13014  isercolllem2  13127  isercolllem3  13128  climsup  13131  caurcvg  13138  caurcvg2  13139  caucvg  13140  infcvgaux1i  13302  mertenslem2  13328  ruclem11  13505  divalglem2  13582  gcdcllem1  13678  bezoutlem2  13706  pclem  13888  pc2dvds  13928  prmreclem1  13960  prmreclem6  13965  4sqlem13  14001  vdwmc2  14023  vdwlem6  14030  vdwlem8  14032  vdwnnlem3  14041  ramtcl  14054  mrcflem  14527  mrcval  14531  iscatd2  14602  fpwipodrs  15317  gsumval2  15493  grpbn0  15547  issubgrpd2  15677  issubg3  15679  issubg4  15680  subgint  15685  cycsubgcl  15687  nmzsubg  15702  ghmpreima  15748  brgici  15778  gastacl  15807  odlem2  16022  gexlem2  16061  sylow1lem5  16081  pgpssslw  16093  sylow2alem2  16097  sylow2blem3  16101  fislw  16104  sylow3lem3  16108  sylow3lem4  16109  torsubg  16316  oddvdssubg  16317  iscygd  16344  iscygodd  16345  cyggexb  16355  gsumval3OLD  16362  gsumval3  16365  dprdsubg  16495  ablfacrp2  16542  ablfac1c  16546  ablfac1eu  16548  pgpfaclem2  16557  subrgugrp  16808  cntzsubr  16821  islss4  16965  lss1d  16966  lssintcl  16967  brlmici  17072  lspsolvlem  17145  lbsextlem1  17161  lidlsubg  17219  abvn0b  17296  psrbas  17382  psrbasOLD  17383  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  ltbwe  17486  mplind  17516  ply1plusgfvi  17595  cnsubglem  17706  cnmsubglem  17719  zringlpirlem1  17745  zlpirlem1  17750  ocvlss  17939  lmiclbs  18108  lmisfree  18113  cramerimplem2  18332  cramerimplem3  18333  cramerimp  18334  clscld  18493  clsval2  18496  lmmo  18826  1stcfb  18891  2ndcdisj  18902  2ndcsep  18905  ptclsg  19030  dfac14lem  19032  txindis  19049  hmphi  19192  opnfbas  19257  trfbas2  19258  isfil2  19271  filn0  19277  zfbas  19311  filssufilg  19326  rnelfmlem  19367  flimclslem  19399  flimfnfcls  19443  ptcmplem2  19467  clssubg  19521  tgpconcomp  19525  tsmsfbas  19540  ustfilxp  19629  ustne0  19630  prdsmet  19787  xbln0  19831  bln0  19832  prdsbl  19908  metustfbasOLD  19982  metustfbas  19983  metustblOLD  19997  metustbl  19998  nrgdomn  20094  nrginvrcn  20114  tgioo  20215  icccmplem2  20242  icccmplem3  20243  reconnlem2  20246  lebnumlem3  20377  phtpcer  20409  reparpht  20412  phtpcco2  20413  pcohtpy  20434  pcorevlem  20440  caun0  20634  iscmet3lem2  20645  bcthlem4  20680  cnflduss  20710  cnfldcusp  20711  reust  20727  recusp  20728  minveclem3b  20757  ivthlem2  20778  ivthlem3  20779  evthicc  20785  ovollb2  20814  ovolctb  20815  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliun2  20831  nulmbl2  20860  ioombl1lem4  20884  uniioombllem1  20903  uniioombllem2  20905  uniioombllem6  20910  mbfsup  20984  mbfinf  20985  mbflimsup  20986  itg1climres  21034  itg2seq  21062  itg2monolem1  21070  itg2mono  21073  itg2i1fseq2  21076  dvferm1lem  21298  dvferm2lem  21300  dvferm  21302  c1liplem1  21310  c1lip1  21311  dvivthlem1  21322  mpfrcl  21370  aannenlem2  21680  aalioulem2  21684  ulm0  21741  pilem2  21802  pilem3  21803  birthdaylem1  22230  ftalem3  22297  ftalem4  22298  ftalem5  22299  dchrabs  22484  pntlem3  22743  tgldimor  22837  axlowdimlem13  23023  axlowdim1  23028  ghgrp  23678  nvo00  23984  nmorepnf  23991  ubthlem1  24094  minvecolem1  24098  shintcl  24556  chintcl  24558  nmoprepnf  25094  nmfnrepnf  25107  nmcexi  25253  snct  25835  submomnd  25997  slmdbn0  26073  slmdsn0  26076  suborng  26136  ordtconlem1  26208  rge0scvg  26233  qqhucn  26275  rrhre  26301  esum0  26357  esumpcvgval  26381  sigagenval  26437  voliune  26499  oddpwdc  26585  eulerpartlemt  26602  erdszelem2  26928  erdszelem8  26934  txsconlem  26977  cvxscon  26980  cvmsss2  27011  cvmliftmolem2  27019  cvmlift2lem12  27051  cvmliftpht  27055  dfrtrcl2  27197  dfso3  27223  sltval2  27644  nocvxminlem  27678  nobndlem5  27684  onint1  28143  heicant  28270  mblfinlem2  28273  ismblfin  28276  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  itg2addnclem  28287  itg2addnc  28290  ftc1anclem7  28317  ftc1anc  28319  finminlem  28357  fnemeet1  28431  fnejoin1  28433  tailfb  28442  incsequz  28488  isbnd3  28527  ssbnd  28531  totbndbnd  28532  prdsbnd  28536  prdsbnd2  28538  heibor1lem  28552  prtlem100  28845  prter3  28872  nacsfix  28893  mzpcln0  28909  rencldnfilem  29004  rencldnfi  29005  fnwe2lem2  29249  kelac1  29261  harn0  29303  hbtlem2  29325  rzalf  29584  ubelsupr  29587  climinf  29625  stoweidlem11  29652  stoweidlem31  29672  stoweidlem34  29675  stoweidlem36  29677  stoweidlem59  29700  stirlinglem13  29727  2reu4  29860  elfvmptrab1  30000  elovmpt3imp  30006  2wlkonot3v  30240  2spthonot3v  30241  usg2spthonot  30253  usg2spthonot0  30254  2spot2iun2spont  30256  clwwlknprop  30281  frg2wotn0  30495  01eq0rng  30608  lincolss  30677  abln0  30733  rngn0  30737  lmodn0  30746  bnj906  31625  bnj1177  31699  bnj1523  31764  bj-tagn0  32055  lkrlss  32313  ishlat3N  32572  hlsupr2  32604  elpaddri  33019  pclvalN  33107  dian0  34257  diaintclN  34276  docaclN  34342  dibintclN  34385  dicn0  34410  dihglblem5  34516  dihglb2  34560  dihintcl  34562  doch2val2  34582  dochocss  34584  lclkr  34751  lclkrs  34757  lcfr  34803  taupi  35190