Theorem ne0i 4287

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  ∅c0 4279

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 3902  df-nul 4280

This theorem is used by:  ne0d  4288  ne0ii  4290  inelcm  4418  rzalALT  4451  2reu4  4480  tpnzd  4741  issn  4792  brne0  5155  ord0eln0  6414  elfvunirn  6908  elfvmptrab1  7015  elovmpt3imp  7671  onnmin  7797  f1oweALT  7969  brovpreldm  8086  bropopvvv  8087  frxp  8124  mpoxopxnop0  8213  brovex  8220  ord1eln01  8483  ord2eln012  8484  oe1m  8532  oa00  8546  oarec  8549  omord  8555  omeulem1  8569  oewordri  8580  oeordsuc  8582  oelim2  8583  nnmord  8620  curfv  8871  map0g  8891  ixpn0  8937  unblem1  9262  wofib  9517  canthwdom  9551  inf1  9601  oemapvali  9663  cantnf  9672  epfrs  9710  acnrcl  10045  iunfictbso  10117  dfac5lem2  10127  kmlem6  10158  fin23lem40  10353  isf34lem7  10381  isf34lem6  10382  fin1a2lem7  10408  fin1a2lem13  10414  alephval2  10581  tskpr  10779  inar1  10784  tskuni  10792  tskxp  10796  tskmap  10797  grur1  10829  axgroth3  10840  inaprc  10845  addclpi  10901  indpi  10916  nqerf  10939  genpn0  11012  infrelb  12224  infssuzle  12980  eliooxr  13457  iccssioo2  13472  iccsupr  13495  elfzoel1  13712  elfzoel2  13713  fzon0  13733  fseqsupubi  14042  hashnn0n0nn  14455  pfxn0  14756  r19.2uz  15439  climuni  15639  ruclem11  16328  bezoutlem2  16630  lcmgcdlem  16696  prmreclem6  17013  vdwlem8  17080  ramtcl  17102  catcone0  17775  fpwipodrs  18628  gsumval2  18788  mgm2nsgrplem1  19030  sgrp2nmndlem1  19035  issubg3  19268  brgici  19398  odlem2  19666  gexlem2  19709  sylow3lem3  19756  abln0  19994  cyggexb  20026  gsumval3  20034  ablfacrp2  20196  ablfac1c  20200  pgpfaclem2  20211  ringn0  20453  brrici  20657  01eq0ringOLD  20692  subrgugrp  20753  brlmici  21253  mpllsslem  22214  ltbwe  22260  mpfrcl  22301  ply1plusgfvi  22466  ply1frcl  22543  cramerimplem2  22909  cramerimplem3  22910  cramerimp  22911  clsval2  23275  lmmo  23605  1stcfb  23670  2ndcsep  23685  ptclsg  23841  txindis  23860  hmphi  24003  trfbas2  24069  flimclslem  24210  ustfilxp  24439  prdsmet  24596  prdsbl  24717  tgioo  25022  caun0  25509  ovolctb  25718  mbflimsup  25894  itg1climres  25942  itg2i1fseq2  25984  dvferm1lem  26211  dvferm2lem  26213  dvferm  26215  c1liplem1  26223  dvivthlem1  26235  aalioulem2  26569  birthdaylem1  27188  ltsval2  27892  nobdaymin  28018  tgldimor  28844  perpin  29079  axlowdimlem13  29411  uvtx01vtx  29857  wlkreslem  30127  wspniunwspnon  30391  usgr2wspthons3  30435  rusgrnumwwlks  30445  rusgrnumwwlk  30446  frgr2wwlkn0  30808  numclwwlk1  30841  numclwlk1lem1  30849  numclwwlk3  30865  numclwwlk5  30868  ubthlem1  31351  n0nsnel  32990  eldmne0  33100  drgextlsp  34104  dimval  34111  dimvalfi  34112  zarcls1  34379  rge0scvg  34459  qqhucn  34502  voliune  34740  eulerpartlemt  34882  dfscott3  35626  erdszelem2  35771  dfso3  36299  fnemeet1  36985  fnejoin1  36987  tailfb  36996  ttc0elw  37146  ttc0el  37154  ptrecube  38369  poimirlem23  38392  poimirlem31  38400  poimirlem32  38401  mblfinlem2  38407  ismblfin  38410  ovoliunnfl  38411  voliunnfl  38413  itg2addnc  38423  totbndbnd  38539  prdsbnd  38543  heibor1lem  38559  eldisjdmqsim  39565  prtlem100  39732  prter3  39755  ishlat3N  40227  hlsupr2  40260  elpaddri  40675  diaintclN  41931  dibintclN  42040  dihintcl  42217  unitscyglem4  43064  rencldnfi  43662  omlimcl2  44083  oaun3lem1  44215  neik0imk0p  44876  clsk3nimkb  44880  amgm3d  45039  amgm4d  45040  prmunb2  45135  rzalf  45851  pwfin0  45896  ssuzfz  46179  fsumiunss  46405  limsupvaluz2  46566  supcnvlimsup  46568  jumpncnp  46726  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem11  46839  stoweidlem31  46859  stoweidlem34  46862  stoweidlem59  46887  fourierdlem31  46966  fourierdlem42  46977  fourierdlem64  46998  fourierdlem73  47007  fourierdlem79  47013  qndenserrnbllem  47122  qndenserrn  47127  sge0rnn0  47196  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem4  47426  ovnlecvr2  47438  hspmbllem2  47455  vonioo  47510  vonicc  47513  smflimsuplem1  47648  smflimsuplem2  47649  n0nsn2el  47913  clnbgrn0  48748  brgrici  48829  brgrilci  48921  cznrng  49176  lmodn0  49425  inisegn0a  49764  elfvne0  49777  lanrcl  50547  ranrcl  50548  rellan  50549  relran  50550  aacllem  50772  amgmw2d  50822