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

Theorem ne0ii 3882
Description: If a set has elements, then it is not empty. Inference associated with ne0i 3880. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
n0ii.1 𝐴𝐵
Assertion
Ref Expression
ne0ii 𝐵 ≠ ∅

Proof of Theorem ne0ii
StepHypRef Expression
1 n0ii.1 . 2 𝐴𝐵
2 ne0i 3880 . 2 (𝐴𝐵𝐵 ≠ ∅)
31, 2ax-mp 5 1 𝐵 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  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:  vn0  3883  prnz  4253  tpnz  4256  pwne0  4761  onn0  5706  oawordeulem  7521  noinfep  8440  fin23lem31  9048  isfin1-3  9091  omina  9392  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  rexfiuz  13935  caurcvg  14255  caurcvg2  14256  caucvg  14257  infcvgaux1i  14428  divalglem2  14956  pc2dvds  15421  vdwmc2  15521  cnsubglem  19614  cnmsubglem  19628  pmatcollpw3  20408  zfbas  21510  nrginvrcn  22306  lebnumlem3  22570  caun0  22887  cnflduss  22960  cnfldcusp  22961  reust  22977  recusp  22978  nulmbl2  23111  itg2seq  23315  itg2monolem1  23323  c1lip1  23564  aannenlem2  23888  logbmpt  24326  tgcgr4  25226  shintcl  27573  chintcl  27575  nmoprepnf  28110  nmfnrepnf  28123  nmcexi  28269  snct  28874  esum0  29438  esumpcvgval  29467  bnj906  30254  bj-tagn0  32160  taupi  32346  ismblfin  32620  volsupnfl  32624  itg2addnclem  32631  ftc1anc  32663  incsequz  32714  isbnd3  32753  ssbnd  32757  corclrcl  37018  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  amgm2d  37523  nnn0  38536  ioodvbdlimc1  38823  ioodvbdlimc2  38825  stirlinglem13  38979  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  hoicvr  39438  2zlidl  41724
  Copyright terms: Public domain W3C validator