Theorem ne0ii 3923

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

Syntax hints:   ∈ wcel 1990   ≠ wne 2794  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  vn0  3924  prnz  4310  tpnz  4313  pwne0  4835  onn0  5789  oawordeulem  7634  noinfep  8557  fin23lem31  9165  isfin1-3  9208  omina  9513  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  rexfiuz  14087  caurcvg  14407  caurcvg2  14408  caucvg  14409  infcvgaux1i  14589  divalglem2  15118  pc2dvds  15583  vdwmc2  15683  cnsubglem  19795  cnmsubglem  19809  pmatcollpw3  20589  zfbas  21700  nrginvrcn  22496  lebnumlem3  22762  caun0  23079  cnflduss  23152  cnfldcusp  23153  reust  23169  recusp  23170  nulmbl2  23304  itg2seq  23509  itg2monolem1  23517  c1lip1  23760  aannenlem2  24084  logbmpt  24526  tgcgr4  25426  shintcl  28189  chintcl  28191  nmoprepnf  28726  nmfnrepnf  28739  nmcexi  28885  snct  29491  esum0  30111  esumpcvgval  30140  bnj906  31000  bj-tagn0  32967  taupi  33169  ismblfin  33450  volsupnfl  33454  itg2addnclem  33461  ftc1anc  33493  incsequz  33544  isbnd3  33583  ssbnd  33587  corclrcl  37999  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  amgm2d  38501  nnn0  39595  ren0  39626  ioodvbdlimc1  40148  ioodvbdlimc2  40150  stirlinglem13  40303  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  hoicvr  40762  2zlidl  41934