Theorem ne0i 4330

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 4329	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neqned 2943	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2936  ∅c0 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-dif 3948  df-nul 4319

This theorem is referenced by:  ne0d  4331  ne0ii  4333  inelcm  4460  rzalALT  4505  rexn0OLD  4510  2reu4  4522  tpnzd  4780  issn  4829  brne0  5192  ord0eln0  6418  elfvunirn  6923  elfvmptrab1  7027  elovmpt3imp  7672  onnmin  7795  f1oweALT  7970  brovpreldm  8088  bropopvvv  8089  frxp  8125  mpoxopxnop0  8214  brovex  8221  ord1eln01  8510  ord2eln012  8511  oe1m  8559  oa00  8573  oarec  8576  omord  8582  omeulem1  8596  oewordri  8606  oeordsuc  8608  oelim2  8609  nnmord  8646  map0g  8896  ixpn0  8942  unblem1  9313  wofib  9562  canthwdom  9596  inf1  9639  oemapvali  9701  cantnf  9710  epfrs  9748  acnrcl  10059  iunfictbso  10131  dfac5lem2  10141  kmlem6  10172  fin23lem40  10368  isf34lem7  10396  isf34lem6  10397  fin1a2lem7  10423  fin1a2lem13  10429  alephval2  10589  tskpr  10787  inar1  10792  tskuni  10800  tskxp  10804  tskmap  10805  grur1  10837  axgroth3  10848  inaprc  10853  addclpi  10909  indpi  10924  nqerf  10947  genpn0  11020  infrelb  12223  infssuzle  12939  eliooxr  13408  iccssioo2  13423  iccsupr  13445  elfzoel1  13656  elfzoel2  13657  fzon0  13676  fseqsupubi  13969  hashnn0n0nn  14376  pfxn0  14662  r19.2uz  15324  climuni  15522  ruclem11  16210  bezoutlem2  16509  lcmgcdlem  16570  prmreclem6  16883  vdwlem8  16950  ramtcl  16972  catcone0  17660  fpwipodrs  18525  gsumval2  18639  mgm2nsgrplem1  18863  sgrp2nmndlem1  18868  issubg3  19092  brgici  19218  odlem2  19487  gexlem2  19530  sylow3lem3  19577  abln0  19815  cyggexb  19847  gsumval3  19855  ablfacrp2  20017  ablfac1c  20021  pgpfaclem2  20032  ringn0  20240  brrici  20437  01eq0ringOLD  20461  subrgugrp  20523  brlmici  20947  mpllsslem  21935  ltbwe  21975  mpfrcl  22024  ply1plusgfvi  22153  ply1frcl  22230  cramerimplem2  22579  cramerimplem3  22580  cramerimp  22581  clsval2  22947  lmmo  23277  1stcfb  23342  2ndcsep  23356  ptclsg  23512  txindis  23531  hmphi  23674  trfbas2  23740  flimclslem  23881  ustfilxp  24110  prdsmet  24269  prdsbl  24393  tgioo  24705  caun0  25202  ovolctb  25412  mbflimsup  25588  itg1climres  25637  itg2i1fseq2  25679  dvferm1lem  25909  dvferm2lem  25911  dvferm  25913  c1liplem1  25922  dvivthlem1  25934  aalioulem2  26261  birthdaylem1  26876  sltval2  27582  tgldimor  28299  axlowdimlem13  28758  uvtx01vtx  29203  wlkreslem  29476  wspniunwspnon  29727  usgr2wspthons3  29768  rusgrnumwwlks  29778  rusgrnumwwlk  29779  frgr2wwlkn0  30131  numclwwlk1  30164  numclwlk1lem1  30172  numclwwlk3  30188  numclwwlk5  30191  ubthlem1  30673  eldmne0  32406  drgextlsp  33283  dimval  33288  dimvalfi  33289  zarcls1  33464  rge0scvg  33544  qqhucn  33587  voliune  33842  eulerpartlemt  33985  erdszelem2  34796  dfso3  35308  fnemeet1  35844  fnejoin1  35846  tailfb  35855  curfv  37067  ptrecube  37087  poimirlem23  37110  poimirlem31  37118  poimirlem32  37119  mblfinlem2  37125  ismblfin  37128  ovoliunnfl  37129  voliunnfl  37131  itg2addnc  37141  totbndbnd  37256  prdsbnd  37260  heibor1lem  37276  prtlem100  38325  prter3  38348  ishlat3N  38820  hlsupr2  38854  elpaddri  39269  diaintclN  40525  dibintclN  40634  dihintcl  40811  rencldnfi  42235  omlimcl2  42664  oaun3lem1  42797  neik0imk0p  43460  clsk3nimkb  43464  amgm3d  43623  amgm4d  43624  prmunb2  43742  rzalf  44373  pwfin0  44420  ssuzfz  44725  fsumiunss  44957  limsupvaluz2  45120  supcnvlimsup  45122  jumpncnp  45280  ioodvbdlimc1lem2  45314  ioodvbdlimc2lem  45316  stoweidlem11  45393  stoweidlem31  45413  stoweidlem34  45416  stoweidlem59  45441  fourierdlem31  45520  fourierdlem42  45531  fourierdlem48  45536  fourierdlem49  45537  fourierdlem64  45552  fourierdlem73  45561  fourierdlem79  45567  qndenserrnbllem  45676  qndenserrn  45681  sge0rnn0  45750  hoidmvlelem1  45977  hoidmvlelem2  45978  hoidmvlelem4  45980  ovnlecvr2  45992  hspmbllem2  46009  vonioo  46064  vonicc  46067  smflimsuplem1  46202  smflimsuplem2  46203  n0nsn2el  46401  brgrici  47174  cznrng  47317  lmodn0  47557  elfvne0  47895  aacllem  48228  amgmw2d  48231