MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ne0i Structured version   Visualization version   GIF version

Theorem ne0i 3879
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
StepHypRef Expression
1 n0i 3878 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 2788 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wne 2779  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-v 3174  df-dif 3542  df-nul 3874
This theorem is referenced by:  ne0ii  3881  inelcm  3983  rzal  4024  rexn0  4025  snnzg  4250  prnzg  4253  tpnzd  4256  brne0  4626  exss  4852  ord0eln0  5682  elfvdm  6115  elfvmptrab1  6198  isofrlem  6468  elovmpt3imp  6765  onnmin  6872  f1oweALT  7020  brovpreldm  7118  bropopvvv  7119  frxp  7151  mpt2xopxnop0  7205  brovex  7212  fvmpt2curryd  7261  onnseq  7305  oe1m  7489  oa00  7503  oarec  7506  omord  7512  oewordri  7536  oeordsuc  7538  oelim2  7539  oeoalem  7540  oeoelem  7542  oeeui  7546  nnmord  7576  nnawordex  7581  map0g  7760  ixpn0  7803  omxpenlem  7923  frfi  8067  unblem1  8074  supgtoreq  8236  infltoreq  8268  wofib  8310  canthwdom  8344  inf1  8379  oemapvali  8441  cantnflem1a  8442  cantnflem1d  8445  cantnflem1  8446  cantnf  8450  epfrs  8467  acnrcl  8725  iunfictbso  8797  dfac5lem2  8807  dfac9  8818  kmlem6  8837  fin23lem40  9033  isf34lem7  9061  isf34lem6  9062  fin1a2lem7  9088  fin1a2lem13  9094  axdc3lem4  9135  alephval2  9250  intwun  9413  r1limwun  9414  tskpr  9448  inar1  9453  tskuni  9461  tskxp  9465  tskmap  9466  gruina  9496  grur1a  9497  grur1  9498  axgroth3  9509  inaprc  9514  addclpi  9570  mulclpi  9571  indpi  9585  nqerf  9608  genpn0  9681  supsrlem  9788  axpre-sup  9846  infrelb  10855  supfirege  10856  uzn0  11535  infssuzle  11603  suprzub  11611  eliooxr  12059  iccssioo2  12073  iccsupr  12093  fzn0  12181  elfzoel1  12292  elfzoel2  12293  fzon0  12311  flval3  12433  icopnfsup  12481  fseqsupubi  12594  hashnn0n0nn  12993  swrdn0  13228  dfrtrcl2  13596  sqrlem3  13779  r19.2uz  13885  climuni  14077  isercolllem2  14190  isercolllem3  14191  climsup  14194  mertenslem2  14402  ruclem11  14754  gcdcllem1  15005  bezoutlem2  15041  lcmgcdlem  15103  pclem  15327  prmreclem1  15404  prmreclem6  15409  4sqlem13  15445  vdwmc2  15467  vdwlem6  15474  vdwlem8  15476  vdwnnlem3  15485  ramtcl  15498  prmgaplem3  15541  prmgaplem4  15542  mrcflem  16035  mrcval  16039  iscatd2  16111  fpwipodrs  16933  gsumval2  17049  mgm2nsgrplem1  17174  sgrp2nmndlem1  17179  grpbn0  17220  issubgrpd2  17379  issubg3  17381  issubg4  17382  subgint  17387  cycsubgcl  17389  nmzsubg  17404  ghmpreima  17451  brgici  17481  gastacl  17511  odlem2  17727  gexlem2  17766  sylow1lem5  17786  pgpssslw  17798  sylow2alem2  17802  sylow2blem3  17806  fislw  17809  sylow3lem3  17813  sylow3lem4  17814  torsubg  18026  oddvdssubg  18027  abln0  18039  iscygd  18058  iscygodd  18059  cyggexb  18069  gsumval3  18077  dprdsubg  18192  ablfacrp2  18235  ablfac1c  18239  ablfac1eu  18241  pgpfaclem2  18250  ringn0  18372  subrgugrp  18568  cntzsubr  18581  islss4  18729  lss1d  18730  lssintcl  18731  brlmici  18836  lspsolvlem  18909  lbsextlem1  18925  lidlsubg  18982  01eq0ring  19039  abvn0b  19069  psrbas  19145  mplsubglem  19201  mpllsslem  19202  ltbwe  19239  mplind  19269  mpfrcl  19285  ply1plusgfvi  19379  ply1frcl  19450  zringlpirlem1  19597  ocvlss  19777  lmiclbs  19937  lmisfree  19942  mat1ric  20054  dmatsgrp  20066  scmatsgrp  20086  scmatsgrp1  20089  scmatlss  20092  scmatric  20104  cramerimplem2  20251  cramerimplem3  20252  cramerimp  20253  cpmatsubgpmat  20286  matcpmric  20325  pmmpric  20389  clscld  20603  clsval2  20606  lmmo  20936  1stcfb  21000  2ndcdisj  21011  2ndcsep  21014  ptclsg  21170  dfac14lem  21172  txindis  21189  hmphi  21332  opnfbas  21398  trfbas2  21399  isfil2  21412  filn0  21418  filssufilg  21467  rnelfmlem  21508  flimclslem  21540  flimfnfcls  21584  ptcmplem2  21609  clssubg  21664  tgpconcomp  21668  tsmsfbas  21683  ustfilxp  21768  ustne0  21769  prdsmet  21926  xbln0  21970  bln0  21971  prdsbl  22047  metustfbas  22113  metustbl  22122  nrgdomn  22218  tgioo  22339  icccmplem2  22366  icccmplem3  22367  reconnlem2  22370  phtpcer  22533  phtpcerOLD  22534  reparpht  22537  phtpcco2  22538  pcohtpy  22559  pcorevlem  22565  isclmp  22636  caun0  22805  iscmet3lem2  22816  bcthlem4  22849  minveclem3b  22924  ivthlem2  22945  ivthlem3  22946  evthicc  22952  ovollb2  22981  ovolctb  22982  ovolunlem1a  22988  ovolunlem1  22989  ovoliunlem1  22994  ovoliun2  22998  ioombl1lem4  23053  uniioombllem1  23072  uniioombllem2  23074  uniioombllem6  23079  mbfsup  23154  mbfinf  23155  mbflimsup  23156  itg1climres  23204  itg2monolem1  23240  itg2mono  23243  itg2i1fseq2  23246  dvferm1lem  23468  dvferm2lem  23470  dvferm  23472  c1liplem1  23480  dvivthlem1  23492  aalioulem2  23809  ulm0  23866  pilem2  23927  pilem3  23928  birthdaylem1  24395  ftalem3  24518  ftalem4  24519  ftalem5  24520  dchrabs  24702  pntlem3  25015  tgldimor  25114  tglnne0  25253  axlowdimlem13  25552  axlowdim1  25557  clwwlknprop  26066  2wlkonot3v  26168  2spthonot3v  26169  usg2spthonot  26181  usg2spthonot0  26182  2spot2iun2spont  26184  frg2wotn0  26349  nvo00  26806  nmorepnf  26813  ubthlem1  26916  minvecolem1  26920  submomnd  28847  slmdbn0  28898  slmdsn0  28901  suborng  28952  ordtconlem1  29104  rge0scvg  29129  qqhucn  29170  rrhre  29199  sigagenval  29336  voliune  29425  oddpwdc  29549  eulerpartlemt  29566  bnj1177  30134  bnj1523  30199  erdszelem2  30234  erdszelem8  30240  txsconlem  30282  cvxscon  30285  cvmsss2  30316  cvmliftmolem2  30324  cvmlift2lem12  30356  cvmliftpht  30360  dfso3  30662  sltval2  30859  nocvxminlem  30895  nobndlem5  30901  finminlem  31288  fnemeet1  31337  fnejoin1  31339  tailfb  31348  onint1  31424  finxpreclem4  32203  curfv  32355  ptrecube  32375  poimirlem23  32398  poimirlem31  32406  poimirlem32  32407  heicant  32410  mblfinlem2  32413  ismblfin  32416  ovoliunnfl  32417  voliunnfl  32419  itg2addnc  32430  ftc1anclem7  32457  ftc1anc  32459  totbndbnd  32554  prdsbnd  32558  prdsbnd2  32560  heibor1lem  32574  prtlem100  32957  prter3  32981  lkrlss  33196  ishlat3N  33455  hlsupr2  33487  elpaddri  33902  pclvalN  33990  dian0  35142  diaintclN  35161  docaclN  35227  dibintclN  35270  dicn0  35295  dihglblem5  35401  dihglb2  35445  dihintcl  35447  doch2val2  35467  dochocss  35469  lclkr  35636  lclkrs  35642  lcfr  35688  nacsfix  36089  mzpcln0  36105  rencldnfilem  36198  rencldnfi  36199  fnwe2lem2  36435  kelac1  36447  harn0  36487  hbtlem2  36509  neik0imk0p  37150  clsk3nimkb  37154  gneispa  37244  amgm3d  37320  amgm4d  37321  prmunb2  37328  rzalf  37995  ubelsupr  37998  pwfin0  38052  suprnmpt  38146  disjinfi  38171  mapdm0  38174  ssfiunibd  38260  ssuzfz  38303  allbutfi  38354  fsumiunss  38439  climinf  38470  limclr  38519  jumpncnp  38581  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc1  38620  ioodvbdlimc2lem  38621  ioodvbdlimc2  38622  stoweidlem11  38701  stoweidlem31  38721  stoweidlem34  38724  stoweidlem36  38726  stoweidlem59  38749  fourierdlem20  38817  fourierdlem25  38822  fourierdlem31  38828  fourierdlem37  38834  fourierdlem42  38839  fourierdlem46  38842  fourierdlem48  38844  fourierdlem49  38845  fourierdlem52  38848  fourierdlem54  38850  fourierdlem64  38860  fourierdlem73  38869  fourierdlem79  38875  fouriercn  38922  elaa2lem  38923  qndenserrnbllem  38987  qndenserrn  38992  salgenval  39014  salgenn0  39022  sge0rnn0  39058  sge0isum  39117  sge0reuzb  39138  ovnlerp  39249  ovnf  39250  hsphoidmvle2  39272  hsphoidmvle  39273  hoiprodp1  39275  hoidmv1lelem1  39278  hoidmv1lelem3  39280  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem4  39285  ovnlecvr2  39297  hoidifhspdmvle  39307  hspmbllem1  39313  hspmbllem2  39314  hspmbllem3  39315  ovnovollem2  39344  vonioo  39370  vonicc  39373  smflimlem1  39454  2reu4  39636  issn  40115  uvtxa01vtx0  40618  1wlkreslem  40873  wspniunwspnon  41125  usgr2wspthons3  41162  rusgrnumwwlks  41172  rusgrnumwwlk  41173  frgr2wwlkn0  41488  av-numclwwlk1  41523  av-numclwwlk3  41534  av-numclwwlk5  41537  cznrng  41742  lincolss  42012  lmodn0  42073  aacllem  42312  amgmw2d  42315
  Copyright terms: Public domain W3C validator