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

Theorem ne0ii 3904
Description: If a set has elements, then it is not empty. Inference associated with ne0i 3902. (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 3902 . 2 (𝐴𝐵𝐵 ≠ ∅)
31, 2ax-mp 5 1 𝐵 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  wne 2790  c0 3896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3191  df-dif 3562  df-nul 3897
This theorem is referenced by:  vn0  3905  prnz  4285  tpnz  4288  pwne0  4800  onn0  5753  oawordeulem  7586  noinfep  8509  fin23lem31  9117  isfin1-3  9160  omina  9465  rpnnen1lem4  11769  rpnnen1lem5  11770  rpnnen1lem4OLD  11775  rpnnen1lem5OLD  11776  rexfiuz  14029  caurcvg  14349  caurcvg2  14350  caucvg  14351  infcvgaux1i  14525  divalglem2  15053  pc2dvds  15518  vdwmc2  15618  cnsubglem  19727  cnmsubglem  19741  pmatcollpw3  20521  zfbas  21623  nrginvrcn  22419  lebnumlem3  22685  caun0  23002  cnflduss  23075  cnfldcusp  23076  reust  23092  recusp  23093  nulmbl2  23227  itg2seq  23432  itg2monolem1  23440  c1lip1  23681  aannenlem2  24005  logbmpt  24443  tgcgr4  25343  shintcl  28059  chintcl  28061  nmoprepnf  28596  nmfnrepnf  28609  nmcexi  28755  snct  29357  esum0  29916  esumpcvgval  29945  bnj906  30743  bj-tagn0  32649  taupi  32837  ismblfin  33117  volsupnfl  33121  itg2addnclem  33128  ftc1anc  33160  incsequz  33211  isbnd3  33250  ssbnd  33254  corclrcl  37515  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37992  amgm2d  38018  nnn0  39090  ren0  39121  ioodvbdlimc1  39481  ioodvbdlimc2  39483  stirlinglem13  39636  fourierdlem103  39759  fourierdlem104  39760  fouriersw  39781  hoicvr  40095  2zlidl  41248
  Copyright terms: Public domain W3C validator