Theorem ne0ii 3735

Description: If a set has elements, then it is not empty. Inference associated with ne0i 3734. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
ne0ii.1	|- A e. B

Assertion

Ref	Expression
ne0ii	|- B =/= (/)

Proof of Theorem ne0ii

Step	Hyp	Ref	Expression
1		ne0ii.1	. 2 |- A e. B
2		ne0i 3734	. 2 |- ( A e. B -> B =/= (/) )
3	1, 2	ax-mp 5	1 |- B =/= (/)

Syntax hints:   e. wcel 1836   =/= wne 2591   (/)c0 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-v 3053  df-dif 3409  df-nul 3729

This theorem is referenced by:  vn0  3736  prnz  4080  tpnz  4082  onn0  4873  oawordeulem  7143  noinfep  8012  fin23lem31  8658  isfin1-3  8701  omina  9002  rpnnen1lem4  11152  rpnnen1lem5  11153  rexfiuz  13205  caurcvg  13524  caurcvg2  13525  caucvg  13526  infcvgaux1i  13693  divalglem2  14078  pc2dvds  14427  vdwmc2  14522  cnsubglem  18603  cnmsubglem  18616  pmatcollpw3  19393  zfbas  20505  nrginvrcn  21308  lebnumlem3  21571  caun0  21828  cnflduss  21904  cnfldcusp  21905  reust  21921  recusp  21922  nulmbl2  22055  itg2seq  22257  itg2monolem1  22265  c1lip1  22506  aannenlem2  22833  logbmpt  23269  shintcl  26390  chintcl  26392  nmoprepnf  26927  nmfnrepnf  26940  nmcexi  27086  snct  27717  esum0  28232  esumpcvgval  28261  ismblfin  30260  volsupnfl  30264  itg2addnclem  30272  ftc1anc  30304  incsequz  30447  isbnd3  30486  ssbnd  30490  ioodvbdlimc1  31935  ioodvbdlimc2  31937  dvnprodlem3  31950  stirlinglem13  32073  fourierdlem103  32197  fourierdlem104  32198  fouriersw  32219  2zlidl  32979  bnj906  34374  bj-tagn0  34924  taupi  38150  corclrcl  38287  imo72b2lem0  38550  imo72b2lem2  38552  imo72b2lem1  38556  imo72b2  38561