Theorem ne0ii 4272

Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4269. (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 4269	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≠ ∅

Syntax hints:   ∈ wcel 2107   ≠ wne 2944  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-dif 3891  df-nul 4258

This theorem is referenced by:  vn0ALT  4274  prnz  4714  tpnz  4716  pwne0  5280  onn0  6334  oawordeulem  8394  noinfep  9427  fin23lem31  10108  isfin1-3  10151  omina  10456  nnunb  12238  rpnnen1lem4  12729  rpnnen1lem5  12730  rexfiuz  15068  caurcvg  15397  caurcvg2  15398  caucvg  15399  infcvgaux1i  15578  divalglem2  16113  pc2dvds  16589  vdwmc2  16689  cnsubglem  20656  cnmsubglem  20670  pmatcollpw3  21942  zfbas  23056  nrginvrcn  23865  lebnumlem3  24135  caun0  24454  cnflduss  24529  cnfldcusp  24530  reust  24554  recusp  24555  nulmbl2  24709  itg2seq  24916  itg2monolem1  24924  c1lip1  25170  aannenlem2  25498  logbmpt  25947  tgcgr4  26901  shintcl  29701  chintcl  29703  nmoprepnf  30238  nmfnrepnf  30251  nmcexi  30397  snct  31057  esum0  32026  esumpcvgval  32055  bnj906  32919  satf0  33343  fmla1  33358  prv0  33401  bj-tagn0  35178  taupi  35503  ismblfin  35827  volsupnfl  35831  itg2addnclem  35837  ftc1anc  35867  incsequz  35915  isbnd3  35951  ssbnd  35955  corclrcl  41322  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2lem1  41787  imo72b2  41790  amgm2d  41816  nnn0  42924  ren0  42949  ioodvbdlimc1  43481  ioodvbdlimc2  43483  stirlinglem13  43634  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  hoicvr  44093  2zlidl  45503