Theorem ne0ii 4123

Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4120. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
n0ii.1	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
ne0ii	⊢ 𝐵 ≠ ∅

Proof of Theorem ne0ii

Step	Hyp	Ref	Expression
1		n0ii.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		ne0i 4120	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≠ ∅

Syntax hints:   ∈ wcel 2157   ≠ wne 2970  ∅c0 4114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-v 3386  df-dif 3771  df-nul 4115

This theorem is referenced by:  vn0  4124  prnz  4497  tpnz  4499  pwne0  5026  onn0  6004  oawordeulem  7873  noinfep  8806  fin23lem31  9452  isfin1-3  9495  omina  9800  rpnnen1lem4  12061  rpnnen1lem5  12062  rexfiuz  14425  caurcvg  14745  caurcvg2  14746  caucvg  14747  infcvgaux1i  14924  divalglem2  15451  pc2dvds  15913  vdwmc2  16013  cnsubglem  20114  cnmsubglem  20128  pmatcollpw3  20914  zfbas  22025  nrginvrcn  22821  lebnumlem3  23087  caun0  23404  cnflduss  23479  cnfldcusp  23480  reust  23504  recusp  23505  nulmbl2  23641  itg2seq  23847  itg2monolem1  23855  c1lip1  24098  aannenlem2  24422  logbmpt  24867  tgcgr4  25775  shintcl  28707  chintcl  28709  nmoprepnf  29244  nmfnrepnf  29257  nmcexi  29403  snct  30002  esum0  30620  esumpcvgval  30649  bnj906  31510  bj-tagn0  33452  taupi  33661  ismblfin  33932  volsupnfl  33936  itg2addnclem  33942  ftc1anc  33974  incsequz  34024  isbnd3  34063  ssbnd  34067  corclrcl  38771  imo72b2lem0  39236  imo72b2lem2  39238  imo72b2lem1  39242  imo72b2  39246  amgm2d  39272  nnn0  40328  ren0  40358  ioodvbdlimc1  40881  ioodvbdlimc2  40883  stirlinglem13  41035  fourierdlem103  41158  fourierdlem104  41159  fouriersw  41180  hoicvr  41497  2zlidl  42722