Theorem ne0i 4235

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

Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2932  ∅c0 4223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-dif 3856  df-nul 4224

This theorem is referenced by:  ne0d  4236  ne0ii  4238  inelcm  4365  rzalALT  4407  rexn0OLD  4412  2reu4  4424  tpnzd  4682  issn  4729  brne0  5089  ord0eln0  6245  elfvmptrab1  6823  elovmpt3imp  7440  onnmin  7560  f1oweALT  7723  brovpreldm  7835  bropopvvv  7836  frxp  7871  mpoxopxnop0  7935  brovex  7942  oe1m  8251  oa00  8265  oarec  8268  omord  8274  omeulem1  8288  oewordri  8298  oeordsuc  8300  oelim2  8301  nnmord  8338  map0g  8543  ixpn0  8589  unblem1  8901  wofib  9139  canthwdom  9173  inf1  9215  oemapvali  9277  cantnf  9286  epfrs  9325  acnrcl  9621  iunfictbso  9693  dfac5lem2  9703  kmlem6  9734  fin23lem40  9930  isf34lem7  9958  isf34lem6  9959  fin1a2lem7  9985  fin1a2lem13  9991  alephval2  10151  tskpr  10349  inar1  10354  tskuni  10362  tskxp  10366  tskmap  10367  grur1  10399  axgroth3  10410  inaprc  10415  addclpi  10471  indpi  10486  nqerf  10509  genpn0  10582  infrelb  11782  infssuzle  12492  eliooxr  12958  iccssioo2  12973  iccsupr  12995  elfzoel1  13206  elfzoel2  13207  fzon0  13225  fseqsupubi  13516  hashnn0n0nn  13923  pfxn0  14216  r19.2uz  14880  climuni  15078  ruclem11  15764  bezoutlem2  16063  lcmgcdlem  16126  prmreclem6  16437  vdwlem8  16504  ramtcl  16526  catcone0  17144  fpwipodrs  18000  gsumval2  18112  mgm2nsgrplem1  18299  sgrp2nmndlem1  18304  issubg3  18515  brgici  18628  odlem2  18885  gexlem2  18925  sylow3lem3  18972  abln0  19206  cyggexb  19238  gsumval3  19246  ablfacrp2  19408  ablfac1c  19412  pgpfaclem2  19423  ringn0  19575  subrgugrp  19773  brlmici  20060  01eq0ring  20264  mpllsslem  20916  ltbwe  20955  mpfrcl  20999  ply1plusgfvi  21117  ply1frcl  21188  cramerimplem2  21535  cramerimplem3  21536  cramerimp  21537  clsval2  21901  lmmo  22231  1stcfb  22296  2ndcsep  22310  ptclsg  22466  txindis  22485  hmphi  22628  trfbas2  22694  flimclslem  22835  ustfilxp  23064  prdsmet  23222  prdsbl  23343  tgioo  23647  caun0  24132  ovolctb  24341  mbflimsup  24517  itg1climres  24566  itg2i1fseq2  24608  dvferm1lem  24835  dvferm2lem  24837  dvferm  24839  c1liplem1  24847  dvivthlem1  24859  aalioulem2  25180  birthdaylem1  25788  tgldimor  26547  axlowdimlem13  26999  uvtx01vtx  27439  wlkreslem  27711  wspniunwspnon  27961  usgr2wspthons3  28002  rusgrnumwwlks  28012  rusgrnumwwlk  28013  frgr2wwlkn0  28365  numclwwlk1  28398  numclwlk1lem1  28406  numclwwlk3  28422  numclwwlk5  28425  ubthlem1  28905  eldmne0  30636  drgextlsp  31349  dimval  31354  dimvalfi  31355  zarcls1  31487  rge0scvg  31567  qqhucn  31608  voliune  31863  eulerpartlemt  32004  erdszelem2  32821  dfso3  33333  sltval2  33545  fnemeet1  34241  fnejoin1  34243  tailfb  34252  curfv  35443  ptrecube  35463  poimirlem23  35486  poimirlem31  35494  poimirlem32  35495  mblfinlem2  35501  ismblfin  35504  ovoliunnfl  35505  voliunnfl  35507  itg2addnc  35517  totbndbnd  35633  prdsbnd  35637  heibor1lem  35653  prtlem100  36559  prter3  36582  ishlat3N  37054  hlsupr2  37087  elpaddri  37502  diaintclN  38758  dibintclN  38867  dihintcl  39044  rencldnfi  40287  neik0imk0p  41264  clsk3nimkb  41268  amgm3d  41429  amgm4d  41430  prmunb2  41543  rzalf  42174  pwfin0  42224  ssuzfz  42502  fsumiunss  42734  limsupvaluz2  42897  supcnvlimsup  42899  jumpncnp  43057  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  stoweidlem11  43170  stoweidlem31  43190  stoweidlem34  43193  stoweidlem59  43218  fourierdlem31  43297  fourierdlem42  43308  fourierdlem48  43313  fourierdlem49  43314  fourierdlem64  43329  fourierdlem73  43338  fourierdlem79  43344  qndenserrnbllem  43453  qndenserrn  43458  sge0rnn0  43524  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem4  43754  ovnlecvr2  43766  hspmbllem2  43783  vonioo  43838  vonicc  43841  smflimsuplem1  43968  smflimsuplem2  43969  cznrng  45129  lmodn0  45452  elfvne0  45792  aacllem  46119  amgmw2d  46122