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

Theorem ne0ii 4307
Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4304. (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 4304 . 2 (𝐴𝐵𝐵 ≠ ∅)
31, 2ax-mp 5 1 𝐵 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wne 3021  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ne 3022  df-dif 3943  df-nul 4296
This theorem is referenced by:  vn0  4308  prnz  4711  tpnz  4713  pwne0  5254  onn0  6253  oawordeulem  8170  noinfep  9112  fin23lem31  9754  isfin1-3  9797  omina  10102  nnunb  11882  rpnnen1lem4  12369  rpnnen1lem5  12370  rexfiuz  14697  caurcvg  15023  caurcvg2  15024  caucvg  15025  infcvgaux1i  15202  divalglem2  15736  pc2dvds  16205  vdwmc2  16305  cnsubglem  20513  cnmsubglem  20527  pmatcollpw3  21311  zfbas  22423  nrginvrcn  23219  lebnumlem3  23485  caun0  23802  cnflduss  23877  cnfldcusp  23878  reust  23902  recusp  23903  nulmbl2  24055  itg2seq  24261  itg2monolem1  24269  c1lip1  24512  aannenlem2  24836  logbmpt  25282  tgcgr4  26234  shintcl  29024  chintcl  29026  nmoprepnf  29561  nmfnrepnf  29574  nmcexi  29720  snct  30365  esum0  31197  esumpcvgval  31226  bnj906  32091  satf0  32506  fmla1  32521  prv0  32564  bj-tagn0  34178  taupi  34476  ismblfin  34803  volsupnfl  34807  itg2addnclem  34813  ftc1anc  34845  incsequz  34894  isbnd3  34933  ssbnd  34937  corclrcl  39920  imo72b2lem0  40384  imo72b2lem2  40386  imo72b2lem1  40390  imo72b2  40394  amgm2d  40420  nnn0  41515  ren0  41543  ioodvbdlimc1  42086  ioodvbdlimc2  42088  stirlinglem13  42240  fourierdlem103  42363  fourierdlem104  42364  fouriersw  42385  hoicvr  42699  2zlidl  44040
  Copyright terms: Public domain W3C validator