Theorem ne0ii 3740

Description: If a set has elements, then it is not empty. Inference associated with ne0i 3739. (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 3739	. 2 |- ( A e. B -> B =/= (/) )
3	1, 2	ax-mp 5	1 |- B =/= (/)

Syntax hints:   e. wcel 1889   =/= wne 2624   (/)c0 3733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-v 3049  df-dif 3409  df-nul 3734

This theorem is referenced by:  vn0  3741  prnz  4094  tpnz  4096  onn0  5490  oawordeulem  7260  noinfep  8170  fin23lem31  8778  isfin1-3  8821  omina  9121  rpnnen1lem4  11300  rpnnen1lem5  11301  rexfiuz  13422  caurcvg  13754  caurcvgOLD  13755  caurcvg2  13756  caucvg  13757  infcvgaux1i  13927  divalglem2  14385  divalglem2OLD  14386  pc2dvds  14840  vdwmc2  14941  cnsubglem  19029  cnmsubglem  19042  pmatcollpw3  19820  zfbas  20923  nrginvrcn  21706  lebnumlem3  22003  lebnumlem3OLD  22006  caun0  22263  cnflduss  22335  cnfldcusp  22336  reust  22352  recusp  22353  nulmbl2  22502  itg2seq  22712  itg2monolem1  22720  c1lip1  22961  aannenlem2  23297  logbmpt  23737  tgcgr4  24588  shintcl  26995  chintcl  26997  nmoprepnf  27532  nmfnrepnf  27545  nmcexi  27691  snct  28307  esum0  28882  esumpcvgval  28911  bnj906  29753  bj-tagn0  31585  taupi  31736  ismblfin  31993  volsupnfl  31997  itg2addnclem  32005  ftc1anc  32037  incsequz  32089  isbnd3  32128  ssbnd  32132  corclrcl  36311  imo72b2lem0  36620  imo72b2lem2  36622  imo72b2lem1  36626  imo72b2  36630  amgm2d  36661  ioodvbdlimc1  37817  ioodvbdlimc2  37820  dvnprodlem3  37833  stirlinglem13  37958  fourierdlem103  38083  fourierdlem104  38084  fouriersw  38105  hoicvr  38380  2zlidl  40038