Theorem ne0i 4290

Description: If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
ne0i	⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 4289	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neqned 2966	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-dif 4050  df-nul 4282

This theorem is used by:  ne0d  4291  ne0ii  4293  inelcm  4421  rzalALT  4454  2reu4  4483  tpnzd  4743  issn  4792  brne0  5161  ord0eln0  6445  elfvunirn  6946  elfvmptrab1  7053  elovmpt3imp  7710  onnmin  7846  f1oweALT  8018  brovpreldm  8135  bropopvvv  8136  frxp  8175  mpoxopxnop0  8270  brovex  8277  ord1eln01  8542  ord2eln012  8543  oe1m  8591  oa00  8605  oarec  8608  omord  8614  omeulem1  8628  oewordri  8639  oeordsuc  8641  oelim2  8642  nnmord  8679  curfv  8930  map0g  8950  ixpn0  8996  unblem1  9322  wofib  9576  canthwdom  9610  inf1  9660  oemapvali  9722  cantnf  9731  epfrs  9769  acnrcl  10160  iunfictbso  10232  dfac5lem2  10242  kmlem6  10273  fin23lem40  10468  isf34lem7  10496  isf34lem6  10497  fin1a2lem7  10523  fin1a2lem13  10529  alephval2  10696  tskpr  10894  inar1  10899  tskuni  10907  tskxp  10911  tskmap  10912  grur1  10944  axgroth3  10955  inaprc  10960  addclpi  11016  indpi  11031  nqerf  11054  genpn0  11127  infrelb  12342  infssuzle  13098  eliooxr  13575  iccssioo2  13590  iccsupr  13613  elfzoel1  13831  elfzoel2  13832  fzon0  13852  fseqsupubi  14161  hashnn0n0nn  14576  pfxn0  14878  r19.2uz  15563  climuni  15763  ruclem11  16452  bezoutlem2  16757  lcmgcdlem  16825  prmreclem6  17143  vdwlem8  17210  ramtcl  17232  catcone0  17911  fpwipodrs  18764  gsumval2  18925  mgm2nsgrplem1  19167  sgrp2nmndlem1  19172  issubg3  19405  brgici  19536  odlem2  19804  gexlem2  19847  sylow3lem3  19894  abln0  20132  cyggexb  20164  gsumval3  20172  ablfacrp2  20334  ablfac1c  20338  pgpfaclem2  20349  ringn0  20593  brrici  20797  01eq0ringOLD  20833  subrgugrp  20894  brlmici  21395  mpllsslem  22362  ltbwe  22408  mpfrcl  22449  ply1plusgfvi  22614  ply1frcl  22691  cramerimplem2  23057  cramerimplem3  23058  cramerimp  23059  clsval2  23423  lmmo  23753  1stcfb  23818  2ndcsep  23833  ptclsg  23989  txindis  24008  hmphi  24151  trfbas2  24217  flimclslem  24358  ustfilxp  24587  prdsmet  24744  prdsbl  24865  tgioo  25170  caun0  25657  ovolctb  25866  mbflimsup  26042  itg1climres  26090  itg2i1fseq2  26132  dvferm1lem  26359  dvferm2lem  26361  dvferm  26363  c1liplem1  26371  dvivthlem1  26383  aalioulem2  26717  birthdaylem1  27336  ltsval2  28070  nobdaymin  28196  tgldimor  29022  perpin  29257  axlowdimlem13  29589  uvtx01vtx  30035  wlkreslem  30305  wspniunwspnon  30569  usgr2wspthons3  30613  rusgrnumwwlks  30623  rusgrnumwwlk  30624  frgr2wwlkn0  30986  numclwwlk1  31019  numclwlk1lem1  31027  numclwwlk3  31043  numclwwlk5  31046  ubthlem1  31529  n0nsnel  33210  eldmne0  33319  drgextlsp  34337  dimval  34344  dimvalfi  34345  zarcls1  34612  rge0scvg  34692  qqhucn  34735  voliune  34973  eulerpartlemt  35114  dfscott3  35868  elscottn0  35877  erdszelem2  36165  elpssex  36672  dfso3  36700  fnemeet1  37369  fnejoin1  37371  tailfb  37380  ttc0elw  37530  ttc0el  37538  ptrecube  38806  poimirlem23  38829  poimirlem31  38837  poimirlem32  38838  mblfinlem2  38844  ismblfin  38847  ovoliunnfl  38848  voliunnfl  38850  itg2addnc  38860  totbndbnd  38989  prdsbnd  38993  heibor1lem  39009  eldisjdmqsim  40015  prtlem100  40182  prter3  40205  ishlat3N  40677  hlsupr2  40710  elpaddri  41125  diaintclN  42381  dibintclN  42490  dihintcl  42667  unitscyglem4  43514  rencldnfi  44094  omlimcl2  44505  oaun3lem1  44637  neik0imk0p  45297  clsk3nimkb  45301  amgm3d  45460  amgm4d  45461  prmunb2  45556  rzalf  46308  pwfin0  46353  ssuzfz  46634  fsumiunss  46860  limsupvaluz2  47021  supcnvlimsup  47023  jumpncnp  47181  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem11  47294  stoweidlem31  47314  stoweidlem34  47317  stoweidlem59  47342  fourierdlem31  47421  fourierdlem42  47432  fourierdlem64  47453  fourierdlem73  47462  fourierdlem79  47468  qndenserrnbllem  47577  qndenserrn  47582  sge0rnn0  47651  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem4  47881  ovnlecvr2  47893  hspmbllem2  47910  vonioo  47965  vonicc  47968  smflimsuplem1  48103  smflimsuplem2  48104  n0nsn2el  48368  clnbgrn0  49203  brgrici  49284  brgrilci  49376  cznrng  49631  lmodn0  49938  inisegn0a  50278  elfvne0  50291  elovmpoeq  50311  lanrcl  51135  ranrcl  51136  rellan  51137  relran  51138  aacllem  51367  amgmw2d  51417