Theorem ne0i 4291

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

Syntax hints:   → wi 4   ∈ wcel 2141   ≠ wne 2956  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3905  df-nul 4284

This theorem is referenced by:  ne0d  4292  ne0ii  4294  inelcm  4416  rzalALT  4446  2reu4  4475  tpnzd  4736  issn  4787  brne0  5147  ord0eln0  6397  elfvunirn  6892  elfvmptrab1  6999  elovmpt3imp  7648  onnmin  7776  f1oweALT  7948  brovpreldm  8062  bropopvvv  8063  frxp  8100  mpoxopxnop0  8189  brovex  8196  ord1eln01  8459  ord2eln012  8460  oe1m  8508  oa00  8522  oarec  8525  omord  8531  omeulem1  8545  oewordri  8556  oeordsuc  8558  oelim2  8559  nnmord  8596  map0g  8860  ixpn0  8906  unblem1  9230  wofib  9487  canthwdom  9521  inf1  9571  oemapvali  9633  cantnf  9642  epfrs  9680  acnrcl  9992  iunfictbso  10064  dfac5lem2  10074  kmlem6  10106  fin23lem40  10302  isf34lem7  10330  isf34lem6  10331  fin1a2lem7  10357  fin1a2lem13  10363  alephval2  10524  tskpr  10722  inar1  10727  tskuni  10735  tskxp  10739  tskmap  10740  grur1  10772  axgroth3  10783  inaprc  10788  addclpi  10844  indpi  10859  nqerf  10882  genpn0  10955  infrelb  12171  infssuzle  12926  eliooxr  13402  iccssioo2  13417  iccsupr  13440  elfzoel1  13656  elfzoel2  13657  fzon0  13677  fseqsupubi  13985  hashnn0n0nn  14398  pfxn0  14694  r19.2uz  15370  climuni  15570  ruclem11  16263  bezoutlem2  16565  lcmgcdlem  16631  prmreclem6  16948  vdwlem8  17015  ramtcl  17037  catcone0  17710  fpwipodrs  18563  gsumval2  18711  mgm2nsgrplem1  18946  sgrp2nmndlem1  18951  issubg3  19177  brgici  19302  odlem2  19570  gexlem2  19613  sylow3lem3  19660  abln0  19898  cyggexb  19930  gsumval3  19938  ablfacrp2  20100  ablfac1c  20104  pgpfaclem2  20115  ringn0  20348  brrici  20541  01eq0ringOLD  20568  subrgugrp  20628  brlmici  21124  mpllsslem  22039  ltbwe  22085  mpfrcl  22126  ply1plusgfvi  22291  ply1frcl  22369  cramerimplem2  22732  cramerimplem3  22733  cramerimp  22734  clsval2  23098  lmmo  23428  1stcfb  23493  2ndcsep  23507  ptclsg  23663  txindis  23682  hmphi  23825  trfbas2  23891  flimclslem  24032  ustfilxp  24261  prdsmet  24418  prdsbl  24539  tgioo  24844  caun0  25331  ovolctb  25540  mbflimsup  25716  itg1climres  25764  itg2i1fseq2  25806  dvferm1lem  26034  dvferm2lem  26036  dvferm  26038  c1liplem1  26046  dvivthlem1  26058  aalioulem2  26385  birthdaylem1  27004  ltsval2  27708  nobdaymin  27834  tgldimor  28659  axlowdimlem13  29112  uvtx01vtx  29555  wlkreslem  29825  wspniunwspnon  30080  usgr2wspthons3  30124  rusgrnumwwlks  30134  rusgrnumwwlk  30135  frgr2wwlkn0  30487  numclwwlk1  30520  numclwlk1lem1  30528  numclwwlk3  30544  numclwwlk5  30547  ubthlem1  31030  n0nsnel  32674  eldmne0  32790  drgextlsp  33852  dimval  33859  dimvalfi  33860  zarcls1  34127  rge0scvg  34207  qqhucn  34250  voliune  34487  eulerpartlemt  34629  erdszelem2  35503  dfso3  36031  fnemeet1  36687  fnejoin1  36689  tailfb  36698  ttc0elw  36848  ttc0el  36856  curfv  38060  ptrecube  38080  poimirlem23  38103  poimirlem31  38111  poimirlem32  38112  mblfinlem2  38118  ismblfin  38121  ovoliunnfl  38122  voliunnfl  38124  itg2addnc  38134  totbndbnd  38249  prdsbnd  38253  heibor1lem  38269  eldisjdmqsim  39277  prtlem100  39444  prter3  39467  ishlat3N  39939  hlsupr2  39972  elpaddri  40387  diaintclN  41643  dibintclN  41752  dihintcl  41929  unitscyglem4  42776  rencldnfi  43359  omlimcl2  43780  oaun3lem1  43912  neik0imk0p  44573  clsk3nimkb  44577  amgm3d  44736  amgm4d  44737  prmunb2  44848  rzalf  45558  pwfin0  45603  ssuzfz  45886  fsumiunss  46112  limsupvaluz2  46273  supcnvlimsup  46275  jumpncnp  46433  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  stoweidlem11  46546  stoweidlem31  46566  stoweidlem34  46569  stoweidlem59  46594  fourierdlem31  46673  fourierdlem42  46684  fourierdlem64  46705  fourierdlem73  46714  fourierdlem79  46720  qndenserrnbllem  46829  qndenserrn  46834  sge0rnn0  46903  hoidmvlelem1  47130  hoidmvlelem2  47131  hoidmvlelem4  47133  ovnlecvr2  47145  hspmbllem2  47162  vonioo  47217  vonicc  47220  smflimsuplem1  47355  smflimsuplem2  47356  n0nsn2el  47580  clnbgrn0  48415  brgrici  48496  brgrilci  48588  cznrng  48844  lmodn0  49078  inisegn0a  49418  elfvne0  49431  lanrcl  50203  ranrcl  50204  rellan  50205  relran  50206  aacllem  50383  amgmw2d  50386