Theorem ne0ii 3956

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

Syntax hints:   ∈ wcel 2030   ≠ wne 2823  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-nul 3949

This theorem is referenced by:  vn0  3957  prnz  4341  tpnz  4344  pwne0  4865  onn0  5827  oawordeulem  7679  noinfep  8595  fin23lem31  9203  isfin1-3  9246  omina  9551  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  rexfiuz  14131  caurcvg  14451  caurcvg2  14452  caucvg  14453  infcvgaux1i  14633  divalglem2  15165  pc2dvds  15630  vdwmc2  15730  cnsubglem  19843  cnmsubglem  19857  pmatcollpw3  20637  zfbas  21747  nrginvrcn  22543  lebnumlem3  22809  caun0  23125  cnflduss  23198  cnfldcusp  23199  reust  23215  recusp  23216  nulmbl2  23350  itg2seq  23554  itg2monolem1  23562  c1lip1  23805  aannenlem2  24129  logbmpt  24571  tgcgr4  25471  shintcl  28317  chintcl  28319  nmoprepnf  28854  nmfnrepnf  28867  nmcexi  29013  snct  29619  esum0  30239  esumpcvgval  30268  bnj906  31126  bj-tagn0  33092  taupi  33299  ismblfin  33580  volsupnfl  33584  itg2addnclem  33591  ftc1anc  33623  incsequz  33674  isbnd3  33713  ssbnd  33717  corclrcl  38316  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  amgm2d  38818  nnn0  39908  ren0  39939  ioodvbdlimc1  40466  ioodvbdlimc2  40468  stirlinglem13  40621  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  hoicvr  41083  2zlidl  42259