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

Theorem ne0i 3954
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 3953 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 2830 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wne 2823  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  ne0ii  3956  inelcm  4065  rzal  4106  rexn0  4107  snnzg  4339  prnzg  4342  tpnzd  4345  issn  4395  brne0  4735  exss  4961  ord0eln0  5817  elfvdm  6258  elfvmptrab1  6344  isofrlem  6630  elovmpt3imp  6932  onnmin  7045  f1oweALT  7194  brovpreldm  7299  bropopvvv  7300  frxp  7332  mpt2xopxnop0  7386  brovex  7393  fvmpt2curryd  7442  onnseq  7486  oe1m  7670  oa00  7684  oarec  7687  omord  7693  oewordri  7717  oeordsuc  7719  oelim2  7720  oeoalem  7721  oeoelem  7723  oeeui  7727  nnmord  7757  nnawordex  7762  map0g  7939  ixpn0  7982  omxpenlem  8102  frfi  8246  unblem1  8253  supgtoreq  8417  infltoreq  8449  wofib  8491  canthwdom  8525  inf1  8557  oemapvali  8619  cantnflem1a  8620  cantnflem1d  8623  cantnflem1  8624  cantnf  8628  epfrs  8645  acnrcl  8903  iunfictbso  8975  dfac5lem2  8985  dfac9  8996  kmlem6  9015  fin23lem40  9211  isf34lem7  9239  isf34lem6  9240  fin1a2lem7  9266  fin1a2lem13  9272  axdc3lem4  9313  alephval2  9432  intwun  9595  r1limwun  9596  tskpr  9630  inar1  9635  tskuni  9643  tskxp  9647  tskmap  9648  gruina  9678  grur1a  9679  grur1  9680  axgroth3  9691  inaprc  9696  addclpi  9752  mulclpi  9753  indpi  9767  nqerf  9790  genpn0  9863  supsrlem  9970  axpre-sup  10028  infrelb  11046  supfirege  11047  uzn0  11741  infssuzle  11809  suprzub  11817  eliooxr  12270  iccssioo2  12284  iccsupr  12304  fzn0  12393  elfzoel1  12507  elfzoel2  12508  fzon0  12526  flval3  12656  icopnfsup  12704  fseqsupubi  12817  hashnn0n0nn  13218  swrdn0  13476  dfrtrcl2  13846  sqrlem3  14029  r19.2uz  14135  climuni  14327  isercolllem2  14440  isercolllem3  14441  climsup  14444  mertenslem2  14661  ruclem11  15013  gcdcllem1  15268  bezoutlem2  15304  lcmgcdlem  15366  pclem  15590  prmreclem1  15667  prmreclem6  15672  4sqlem13  15708  vdwmc2  15730  vdwlem6  15737  vdwlem8  15739  vdwnnlem3  15748  ramtcl  15761  prmgaplem3  15804  prmgaplem4  15805  mrcflem  16313  mrcval  16317  iscatd2  16389  fpwipodrs  17211  gsumval2  17327  mgm2nsgrplem1  17452  sgrp2nmndlem1  17457  grpbn0  17498  issubgrpd2  17657  issubg3  17659  issubg4  17660  subgint  17665  cycsubgcl  17667  nmzsubg  17682  ghmpreima  17729  brgici  17759  gastacl  17788  odlem2  18004  gexlem2  18043  sylow1lem5  18063  pgpssslw  18075  sylow2alem2  18079  sylow2blem3  18083  fislw  18086  sylow3lem3  18090  sylow3lem4  18091  torsubg  18303  oddvdssubg  18304  abln0  18316  iscygd  18335  iscygodd  18336  cyggexb  18346  gsumval3  18354  dprdsubg  18469  ablfacrp2  18512  ablfac1c  18516  ablfac1eu  18518  pgpfaclem2  18527  ringn0  18649  subrgugrp  18847  cntzsubr  18860  islss4  19010  lss1d  19011  lssintcl  19012  brlmici  19117  lspsolvlem  19190  lbsextlem1  19206  lidlsubg  19263  01eq0ring  19320  abvn0b  19350  psrbas  19426  mplsubglem  19482  mpllsslem  19483  ltbwe  19520  mplind  19550  mpfrcl  19566  ply1plusgfvi  19660  ply1frcl  19731  zringlpirlem1  19880  ocvlss  20064  lmiclbs  20224  lmisfree  20229  mat1ric  20341  dmatsgrp  20353  scmatsgrp  20373  scmatsgrp1  20376  scmatlss  20379  scmatric  20391  cramerimplem2  20538  cramerimplem3  20539  cramerimp  20540  cpmatsubgpmat  20573  matcpmric  20612  pmmpric  20676  clscld  20899  clsval2  20902  lmmo  21232  1stcfb  21296  2ndcdisj  21307  2ndcsep  21310  ptclsg  21466  dfac14lem  21468  txindis  21485  hmphi  21628  opnfbas  21693  trfbas2  21694  isfil2  21707  filn0  21713  filssufilg  21762  rnelfmlem  21803  flimclslem  21835  flimfnfcls  21879  ptcmplem2  21904  clssubg  21959  tgpconncomp  21963  tsmsfbas  21978  ustfilxp  22063  ustne0  22064  prdsmet  22222  xbln0  22266  bln0  22267  prdsbl  22343  metustfbas  22409  metustbl  22418  nrgdomn  22522  tgioo  22646  icccmplem2  22673  icccmplem3  22674  reconnlem2  22677  phtpcer  22841  reparpht  22844  phtpcco2  22845  pcohtpy  22866  pcorevlem  22872  isclmp  22943  caun0  23125  iscmet3lem2  23136  bcthlem4  23170  minveclem3b  23245  ivthlem2  23267  ivthlem3  23268  evthicc  23274  ovollb2  23303  ovolctb  23304  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliun2  23320  ioombl1lem4  23375  uniioombllem1  23395  uniioombllem2  23397  uniioombllem6  23402  mbfsup  23476  mbfinf  23477  mbflimsup  23478  itg1climres  23526  itg2monolem1  23562  itg2mono  23565  itg2i1fseq2  23568  dvferm1lem  23792  dvferm2lem  23794  dvferm  23796  c1liplem1  23804  dvivthlem1  23816  aalioulem2  24133  ulm0  24190  pilem2  24251  pilem3  24252  birthdaylem1  24723  ftalem3  24846  ftalem4  24847  ftalem5  24848  dchrabs  25030  pntlem3  25343  tgldimor  25442  tglnne0  25580  axlowdimlem13  25879  axlowdim1  25884  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  wlkreslem  26622  wspniunwspnon  26888  usgr2wspthons3  26931  rusgrnumwwlks  26941  rusgrnumwwlk  26942  frgr2wwlkn0  27308  numclwwlk1  27351  numclwwlk3  27372  numclwwlk5  27375  nvo00  27744  nmorepnf  27751  ubthlem1  27854  minvecolem1  27858  submomnd  29838  slmdbn0  29889  slmdsn0  29892  suborng  29943  ordtconnlem1  30098  rge0scvg  30123  qqhucn  30164  rrhre  30193  sigagenval  30331  voliune  30420  oddpwdc  30544  eulerpartlemt  30561  bnj1177  31200  bnj1523  31265  erdszelem2  31300  erdszelem8  31306  txsconnlem  31348  cvxsconn  31351  cvmsss2  31382  cvmliftmolem2  31390  cvmlift2lem12  31422  cvmliftpht  31426  dfso3  31727  sltval2  31934  nocvxminlem  32018  finminlem  32437  fnemeet1  32486  fnejoin1  32488  tailfb  32497  onint1  32573  finxpreclem4  33361  curfv  33519  ptrecube  33539  poimirlem23  33562  poimirlem31  33570  poimirlem32  33571  heicant  33574  mblfinlem2  33577  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  itg2addnc  33594  ftc1anclem7  33621  ftc1anc  33623  totbndbnd  33718  prdsbnd  33722  prdsbnd2  33724  heibor1lem  33738  prtlem100  34463  prter3  34486  lkrlss  34700  ishlat3N  34959  hlsupr2  34991  elpaddri  35406  pclvalN  35494  dian0  36645  diaintclN  36664  docaclN  36730  dibintclN  36773  dicn0  36798  dihglblem5  36904  dihglb2  36948  dihintcl  36950  doch2val2  36970  dochocss  36972  lclkr  37139  lclkrs  37145  lcfr  37191  nacsfix  37592  mzpcln0  37608  rencldnfilem  37701  rencldnfi  37702  fnwe2lem2  37938  kelac1  37950  harn0  37989  hbtlem2  38011  neik0imk0p  38651  clsk3nimkb  38655  gneispa  38745  amgm3d  38819  amgm4d  38820  prmunb2  38827  rzalf  39490  ubelsupr  39493  pwfin0  39545  ne0d  39622  suprnmpt  39669  disjinfi  39694  mapdm0OLD  39697  suprubrnmpt2  39781  suprubrnmpt  39782  ssfiunibd  39837  ssuzfz  39878  allbutfi  39929  allbutfiinf  39960  fsumiunss  40125  climinf  40156  limclr  40205  limsupubuzlem  40262  limsupvaluz2  40288  supcnvlimsup  40290  liminflelimsupuz  40335  jumpncnp  40429  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc1  40466  ioodvbdlimc2lem  40467  ioodvbdlimc2  40468  stoweidlem11  40546  stoweidlem31  40566  stoweidlem34  40569  stoweidlem36  40571  stoweidlem59  40594  fourierdlem20  40662  fourierdlem25  40667  fourierdlem31  40673  fourierdlem37  40679  fourierdlem42  40684  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem52  40693  fourierdlem54  40695  fourierdlem64  40705  fourierdlem73  40714  fourierdlem79  40720  fouriercn  40767  elaa2lem  40768  qndenserrnbllem  40832  qndenserrn  40837  salgenval  40859  salgenn0  40867  sge0rnn0  40903  sge0isum  40962  sge0reuzb  40983  ovnlerp  41097  ovnf  41098  hsphoidmvle2  41120  hsphoidmvle  41121  hoiprodp1  41123  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem4  41133  ovnlecvr2  41145  hoidifhspdmvle  41155  hspmbllem1  41161  hspmbllem2  41162  hspmbllem3  41163  ovnovollem2  41192  vonioo  41217  vonicc  41220  smflimlem1  41300  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem5  41351  smflimsuplem7  41353  2reu4  41511  cznrng  42280  lincolss  42548  lmodn0  42609  aacllem  42875  amgmw2d  42878
  Copyright terms: Public domain W3C validator