Theorem ne0i 4281

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-nul 4274

This theorem is referenced by:  ne0d  4282  ne0ii  4284  inelcm  4405  rzalALT  4435  2reu4  4464  tpnzd  4724  issn  4775  brne0  5135  ord0eln0  6379  elfvunirn  6870  elfvmptrab1  6976  elovmpt3imp  7624  onnmin  7752  f1oweALT  7925  brovpreldm  8039  bropopvvv  8040  frxp  8076  mpoxopxnop0  8165  brovex  8172  ord1eln01  8431  ord2eln012  8432  oe1m  8480  oa00  8494  oarec  8497  omord  8503  omeulem1  8517  oewordri  8528  oeordsuc  8530  oelim2  8531  nnmord  8568  map0g  8832  ixpn0  8878  unblem1  9202  wofib  9460  canthwdom  9494  inf1  9543  oemapvali  9605  cantnf  9614  epfrs  9652  acnrcl  9964  iunfictbso  10036  dfac5lem2  10046  kmlem6  10078  fin23lem40  10273  isf34lem7  10301  isf34lem6  10302  fin1a2lem7  10328  fin1a2lem13  10334  alephval2  10495  tskpr  10693  inar1  10698  tskuni  10706  tskxp  10710  tskmap  10711  grur1  10743  axgroth3  10754  inaprc  10759  addclpi  10815  indpi  10830  nqerf  10853  genpn0  10926  infrelb  12141  infssuzle  12881  eliooxr  13357  iccssioo2  13372  iccsupr  13395  elfzoel1  13611  elfzoel2  13612  fzon0  13632  fseqsupubi  13940  hashnn0n0nn  14353  pfxn0  14649  r19.2uz  15314  climuni  15514  ruclem11  16207  bezoutlem2  16509  lcmgcdlem  16575  prmreclem6  16892  vdwlem8  16959  ramtcl  16981  catcone0  17653  fpwipodrs  18506  gsumval2  18654  mgm2nsgrplem1  18889  sgrp2nmndlem1  18894  issubg3  19120  brgici  19246  odlem2  19514  gexlem2  19557  sylow3lem3  19604  abln0  19842  cyggexb  19874  gsumval3  19882  ablfacrp2  20044  ablfac1c  20048  pgpfaclem2  20059  ringn0  20292  brrici  20482  01eq0ringOLD  20508  subrgugrp  20568  brlmici  21064  mpllsslem  21978  ltbwe  22022  mpfrcl  22063  ply1plusgfvi  22205  ply1frcl  22283  cramerimplem2  22649  cramerimplem3  22650  cramerimp  22651  clsval2  23015  lmmo  23345  1stcfb  23410  2ndcsep  23424  ptclsg  23580  txindis  23599  hmphi  23742  trfbas2  23808  flimclslem  23949  ustfilxp  24178  prdsmet  24335  prdsbl  24456  tgioo  24761  caun0  25248  ovolctb  25457  mbflimsup  25633  itg1climres  25681  itg2i1fseq2  25723  dvferm1lem  25951  dvferm2lem  25953  dvferm  25955  c1liplem1  25963  dvivthlem1  25975  aalioulem2  26299  birthdaylem1  26915  ltsval2  27620  nobdaymin  27745  tgldimor  28570  axlowdimlem13  29023  uvtx01vtx  29466  wlkreslem  29736  wspniunwspnon  29991  usgr2wspthons3  30035  rusgrnumwwlks  30045  rusgrnumwwlk  30046  frgr2wwlkn0  30398  numclwwlk1  30431  numclwlk1lem1  30439  numclwwlk3  30455  numclwwlk5  30458  ubthlem1  30941  n0nsnel  32585  eldmne0  32700  drgextlsp  33738  dimval  33745  dimvalfi  33746  zarcls1  34013  rge0scvg  34093  qqhucn  34136  voliune  34373  eulerpartlemt  34515  erdszelem2  35374  dfso3  35902  fnemeet1  36548  fnejoin1  36550  tailfb  36559  ttc0elw  36709  ttc0el  36717  curfv  37921  ptrecube  37941  poimirlem23  37964  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  itg2addnc  37995  totbndbnd  38110  prdsbnd  38114  heibor1lem  38130  eldisjdmqsim  39138  prtlem100  39305  prter3  39328  ishlat3N  39800  hlsupr2  39833  elpaddri  40248  diaintclN  41504  dibintclN  41613  dihintcl  41790  unitscyglem4  42637  rencldnfi  43249  omlimcl2  43670  oaun3lem1  43802  neik0imk0p  44463  clsk3nimkb  44467  amgm3d  44626  amgm4d  44627  prmunb2  44738  rzalf  45448  pwfin0  45493  ssuzfz  45779  fsumiunss  46005  limsupvaluz2  46166  supcnvlimsup  46168  jumpncnp  46326  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem11  46439  stoweidlem31  46459  stoweidlem34  46462  stoweidlem59  46487  fourierdlem31  46566  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem64  46598  fourierdlem73  46607  fourierdlem79  46613  qndenserrnbllem  46722  qndenserrn  46727  sge0rnn0  46796  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem4  47026  ovnlecvr2  47038  hspmbllem2  47055  vonioo  47110  vonicc  47113  smflimsuplem1  47248  smflimsuplem2  47249  n0nsn2el  47473  clnbgrn0  48308  brgrici  48389  brgrilci  48481  cznrng  48737  lmodn0  48971  inisegn0a  49311  elfvne0  49324  lanrcl  50096  ranrcl  50097  rellan  50098  relran  50099  aacllem  50276  amgmw2d  50279