Theorem ne0i 3880

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

Assertion

Ref	Expression
ne0i	⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3879	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neqned 2789	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 1977   ≠ wne 2780  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  ne0ii  3882  inelcm  3984  rzal  4025  rexn0  4026  snnzg  4251  prnzg  4254  tpnzd  4257  issn  4303  brne0  4632  exss  4858  ord0eln0  5696  elfvdm  6130  elfvmptrab1  6213  isofrlem  6490  elovmpt3imp  6788  onnmin  6895  f1oweALT  7043  brovpreldm  7141  bropopvvv  7142  frxp  7174  mpt2xopxnop0  7228  brovex  7235  fvmpt2curryd  7284  onnseq  7328  oe1m  7512  oa00  7526  oarec  7529  omord  7535  oewordri  7559  oeordsuc  7561  oelim2  7562  oeoalem  7563  oeoelem  7565  oeeui  7569  nnmord  7599  nnawordex  7604  map0g  7783  ixpn0  7826  omxpenlem  7946  frfi  8090  unblem1  8097  supgtoreq  8259  infltoreq  8291  wofib  8333  canthwdom  8367  inf1  8402  oemapvali  8464  cantnflem1a  8465  cantnflem1d  8468  cantnflem1  8469  cantnf  8473  epfrs  8490  acnrcl  8748  iunfictbso  8820  dfac5lem2  8830  dfac9  8841  kmlem6  8860  fin23lem40  9056  isf34lem7  9084  isf34lem6  9085  fin1a2lem7  9111  fin1a2lem13  9117  axdc3lem4  9158  alephval2  9273  intwun  9436  r1limwun  9437  tskpr  9471  inar1  9476  tskuni  9484  tskxp  9488  tskmap  9489  gruina  9519  grur1a  9520  grur1  9521  axgroth3  9532  inaprc  9537  addclpi  9593  mulclpi  9594  indpi  9608  nqerf  9631  genpn0  9704  supsrlem  9811  axpre-sup  9869  infrelb  10885  supfirege  10886  uzn0  11579  infssuzle  11647  suprzub  11655  eliooxr  12103  iccssioo2  12117  iccsupr  12137  fzn0  12226  elfzoel1  12337  elfzoel2  12338  fzon0  12356  flval3  12478  icopnfsup  12526  fseqsupubi  12639  hashnn0n0nn  13041  swrdn0  13282  dfrtrcl2  13650  sqrlem3  13833  r19.2uz  13939  climuni  14131  isercolllem2  14244  isercolllem3  14245  climsup  14248  mertenslem2  14456  ruclem11  14808  gcdcllem1  15059  bezoutlem2  15095  lcmgcdlem  15157  pclem  15381  prmreclem1  15458  prmreclem6  15463  4sqlem13  15499  vdwmc2  15521  vdwlem6  15528  vdwlem8  15530  vdwnnlem3  15539  ramtcl  15552  prmgaplem3  15595  prmgaplem4  15596  mrcflem  16089  mrcval  16093  iscatd2  16165  fpwipodrs  16987  gsumval2  17103  mgm2nsgrplem1  17228  sgrp2nmndlem1  17233  grpbn0  17274  issubgrpd2  17433  issubg3  17435  issubg4  17436  subgint  17441  cycsubgcl  17443  nmzsubg  17458  ghmpreima  17505  brgici  17535  gastacl  17565  odlem2  17781  gexlem2  17820  sylow1lem5  17840  pgpssslw  17852  sylow2alem2  17856  sylow2blem3  17860  fislw  17863  sylow3lem3  17867  sylow3lem4  17868  torsubg  18080  oddvdssubg  18081  abln0  18093  iscygd  18112  iscygodd  18113  cyggexb  18123  gsumval3  18131  dprdsubg  18246  ablfacrp2  18289  ablfac1c  18293  ablfac1eu  18295  pgpfaclem2  18304  ringn0  18426  subrgugrp  18622  cntzsubr  18635  islss4  18783  lss1d  18784  lssintcl  18785  brlmici  18890  lspsolvlem  18963  lbsextlem1  18979  lidlsubg  19036  01eq0ring  19093  abvn0b  19123  psrbas  19199  mplsubglem  19255  mpllsslem  19256  ltbwe  19293  mplind  19323  mpfrcl  19339  ply1plusgfvi  19433  ply1frcl  19504  zringlpirlem1  19651  ocvlss  19835  lmiclbs  19995  lmisfree  20000  mat1ric  20112  dmatsgrp  20124  scmatsgrp  20144  scmatsgrp1  20147  scmatlss  20150  scmatric  20162  cramerimplem2  20309  cramerimplem3  20310  cramerimp  20311  cpmatsubgpmat  20344  matcpmric  20383  pmmpric  20447  clscld  20661  clsval2  20664  lmmo  20994  1stcfb  21058  2ndcdisj  21069  2ndcsep  21072  ptclsg  21228  dfac14lem  21230  txindis  21247  hmphi  21390  opnfbas  21456  trfbas2  21457  isfil2  21470  filn0  21476  filssufilg  21525  rnelfmlem  21566  flimclslem  21598  flimfnfcls  21642  ptcmplem2  21667  clssubg  21722  tgpconcomp  21726  tsmsfbas  21741  ustfilxp  21826  ustne0  21827  prdsmet  21985  xbln0  22029  bln0  22030  prdsbl  22106  metustfbas  22172  metustbl  22181  nrgdomn  22285  tgioo  22407  icccmplem2  22434  icccmplem3  22435  reconnlem2  22438  phtpcer  22602  phtpcerOLD  22603  reparpht  22606  phtpcco2  22607  pcohtpy  22628  pcorevlem  22634  isclmp  22705  caun0  22887  iscmet3lem2  22898  bcthlem4  22932  minveclem3b  23007  ivthlem2  23028  ivthlem3  23029  evthicc  23035  ovollb2  23064  ovolctb  23065  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun2  23081  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem2  23157  uniioombllem6  23162  mbfsup  23237  mbfinf  23238  mbflimsup  23239  itg1climres  23287  itg2monolem1  23323  itg2mono  23326  itg2i1fseq2  23329  dvferm1lem  23551  dvferm2lem  23553  dvferm  23555  c1liplem1  23563  dvivthlem1  23575  aalioulem2  23892  ulm0  23949  pilem2  24010  pilem3  24011  birthdaylem1  24478  ftalem3  24601  ftalem4  24602  ftalem5  24603  dchrabs  24785  pntlem3  25098  tgldimor  25197  tglnne0  25335  axlowdimlem13  25634  axlowdim1  25639  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  usg2spthonot  26415  usg2spthonot0  26416  2spot2iun2spont  26418  frg2wotn0  26583  nvo00  27000  nmorepnf  27007  ubthlem1  27110  minvecolem1  27114  submomnd  29041  slmdbn0  29092  slmdsn0  29095  suborng  29146  ordtconlem1  29298  rge0scvg  29323  qqhucn  29364  rrhre  29393  sigagenval  29530  voliune  29619  oddpwdc  29743  eulerpartlemt  29760  bnj1177  30328  bnj1523  30393  erdszelem2  30428  erdszelem8  30434  txsconlem  30476  cvxscon  30479  cvmsss2  30510  cvmliftmolem2  30518  cvmlift2lem12  30550  cvmliftpht  30554  dfso3  30856  sltval2  31053  nocvxminlem  31089  nobndlem5  31095  finminlem  31482  fnemeet1  31531  fnejoin1  31533  tailfb  31542  onint1  31618  finxpreclem4  32407  curfv  32559  ptrecube  32579  poimirlem23  32602  poimirlem31  32610  poimirlem32  32611  heicant  32614  mblfinlem2  32617  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  itg2addnc  32634  ftc1anclem7  32661  ftc1anc  32663  totbndbnd  32758  prdsbnd  32762  prdsbnd2  32764  heibor1lem  32778  prtlem100  33161  prter3  33185  lkrlss  33400  ishlat3N  33659  hlsupr2  33691  elpaddri  34106  pclvalN  34194  dian0  35346  diaintclN  35365  docaclN  35431  dibintclN  35474  dicn0  35499  dihglblem5  35605  dihglb2  35649  dihintcl  35651  doch2val2  35671  dochocss  35673  lclkr  35840  lclkrs  35846  lcfr  35892  nacsfix  36293  mzpcln0  36309  rencldnfilem  36402  rencldnfi  36403  fnwe2lem2  36639  kelac1  36651  harn0  36691  hbtlem2  36713  neik0imk0p  37354  clsk3nimkb  37358  gneispa  37448  amgm3d  37524  amgm4d  37525  prmunb2  37532  rzalf  38199  ubelsupr  38202  pwfin0  38256  suprnmpt  38350  disjinfi  38375  mapdm0  38378  ssfiunibd  38464  ssuzfz  38506  allbutfi  38557  fsumiunss  38642  climinf  38673  limclr  38722  jumpncnp  38784  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  stoweidlem11  38904  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem59  38952  fourierdlem20  39020  fourierdlem25  39025  fourierdlem31  39031  fourierdlem37  39037  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem52  39051  fourierdlem54  39053  fourierdlem64  39063  fourierdlem73  39072  fourierdlem79  39078  fouriercn  39125  elaa2lem  39126  qndenserrnbllem  39190  qndenserrn  39195  salgenval  39217  salgenn0  39225  sge0rnn0  39261  sge0isum  39320  sge0reuzb  39341  ovnlerp  39452  ovnf  39453  hsphoidmvle2  39475  hsphoidmvle  39476  hoiprodp1  39478  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  ovnlecvr2  39500  hoidifhspdmvle  39510  hspmbllem1  39516  hspmbllem2  39517  hspmbllem3  39518  ovnovollem2  39547  vonioo  39573  vonicc  39576  smflimlem1  39657  2reu4  39839  uvtxa01vtx0  40623  1wlkreslem  40878  wspniunwspnon  41130  usgr2wspthons3  41167  rusgrnumwwlks  41177  rusgrnumwwlk  41178  frgr2wwlkn0  41493  av-numclwwlk1  41528  av-numclwwlk3  41539  av-numclwwlk5  41542  cznrng  41747  lincolss  42017  lmodn0  42078  aacllem  42356  amgmw2d  42359