Theorem ne0i 4302

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-dif 3916  df-nul 4295

This theorem is referenced by:  ne0d  4303  ne0ii  4305  inelcm  4428  rzalALT  4458  2reu4  4487  tpnzd  4748  issn  4798  brne0  5162  ord0eln0  6414  elfvunirn  6909  elfvmptrab1  7016  elovmpt3imp  7665  onnmin  7793  f1oweALT  7965  brovpreldm  8080  bropopvvv  8081  frxp  8118  mpoxopxnop0  8207  brovex  8214  ord1eln01  8477  ord2eln012  8478  oe1m  8526  oa00  8540  oarec  8543  omord  8549  omeulem1  8563  oewordri  8574  oeordsuc  8576  oelim2  8577  nnmord  8614  map0g  8878  ixpn0  8924  unblem1  9248  wofib  9503  canthwdom  9537  inf1  9587  oemapvali  9649  cantnf  9658  epfrs  9696  acnrcl  10022  iunfictbso  10094  dfac5lem2  10104  kmlem6  10135  fin23lem40  10331  isf34lem7  10359  isf34lem6  10360  fin1a2lem7  10386  fin1a2lem13  10392  alephval2  10553  tskpr  10751  inar1  10756  tskuni  10764  tskxp  10768  tskmap  10769  grur1  10801  axgroth3  10812  inaprc  10817  addclpi  10873  indpi  10888  nqerf  10911  genpn0  10984  infrelb  12196  infssuzle  12951  eliooxr  13427  iccssioo2  13442  iccsupr  13465  elfzoel1  13681  elfzoel2  13682  fzon0  13702  fseqsupubi  14010  hashnn0n0nn  14423  pfxn0  14720  r19.2uz  15399  climuni  15599  ruclem11  16292  bezoutlem2  16594  lcmgcdlem  16660  prmreclem6  16977  vdwlem8  17044  ramtcl  17066  catcone0  17739  fpwipodrs  18592  gsumval2  18740  mgm2nsgrplem1  18976  sgrp2nmndlem1  18981  issubg3  19207  brgici  19337  odlem2  19605  gexlem2  19648  sylow3lem3  19695  abln0  19933  cyggexb  19965  gsumval3  19973  ablfacrp2  20135  ablfac1c  20139  pgpfaclem2  20150  ringn0  20390  brrici  20583  01eq0ringOLD  20611  subrgugrp  20672  brlmici  21164  mpllsslem  22114  ltbwe  22160  mpfrcl  22201  ply1plusgfvi  22366  ply1frcl  22443  cramerimplem2  22806  cramerimplem3  22807  cramerimp  22808  clsval2  23172  lmmo  23502  1stcfb  23567  2ndcsep  23581  ptclsg  23737  txindis  23756  hmphi  23899  trfbas2  23965  flimclslem  24106  ustfilxp  24335  prdsmet  24492  prdsbl  24613  tgioo  24918  caun0  25405  ovolctb  25614  mbflimsup  25790  itg1climres  25838  itg2i1fseq2  25880  dvferm1lem  26108  dvferm2lem  26110  dvferm  26112  c1liplem1  26120  dvivthlem1  26132  aalioulem2  26459  birthdaylem1  27078  ltsval2  27782  nobdaymin  27908  tgldimor  28733  perpin  28960  axlowdimlem13  29241  uvtx01vtx  29684  wlkreslem  29954  wspniunwspnon  30209  usgr2wspthons3  30253  rusgrnumwwlks  30263  rusgrnumwwlk  30264  frgr2wwlkn0  30616  numclwwlk1  30649  numclwlk1lem1  30657  numclwwlk3  30673  numclwwlk5  30676  ubthlem1  31159  n0nsnel  32798  eldmne0  32909  drgextlsp  33925  dimval  33932  dimvalfi  33933  zarcls1  34200  rge0scvg  34280  qqhucn  34323  voliune  34560  eulerpartlemt  34702  erdszelem2  35579  dfso3  36107  fnemeet1  36762  fnejoin1  36764  tailfb  36773  ttc0elw  36923  ttc0el  36931  curfv  38134  ptrecube  38154  poimirlem23  38177  poimirlem31  38185  poimirlem32  38186  mblfinlem2  38192  ismblfin  38195  ovoliunnfl  38196  voliunnfl  38198  itg2addnc  38208  totbndbnd  38323  prdsbnd  38327  heibor1lem  38343  eldisjdmqsim  39351  prtlem100  39518  prter3  39541  ishlat3N  40013  hlsupr2  40046  elpaddri  40461  diaintclN  41717  dibintclN  41826  dihintcl  42003  unitscyglem4  42850  rencldnfi  43433  omlimcl2  43854  oaun3lem1  43986  neik0imk0p  44647  clsk3nimkb  44651  amgm3d  44810  amgm4d  44811  prmunb2  44906  rzalf  45622  pwfin0  45667  ssuzfz  45950  fsumiunss  46176  limsupvaluz2  46337  supcnvlimsup  46339  jumpncnp  46497  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  stoweidlem11  46610  stoweidlem31  46630  stoweidlem34  46633  stoweidlem59  46658  fourierdlem31  46737  fourierdlem42  46748  fourierdlem64  46769  fourierdlem73  46778  fourierdlem79  46784  qndenserrnbllem  46893  qndenserrn  46898  sge0rnn0  46967  hoidmvlelem1  47194  hoidmvlelem2  47195  hoidmvlelem4  47197  ovnlecvr2  47209  hspmbllem2  47226  vonioo  47281  vonicc  47284  smflimsuplem1  47419  smflimsuplem2  47420  n0nsn2el  47644  clnbgrn0  48479  brgrici  48560  brgrilci  48652  cznrng  48908  lmodn0  49153  inisegn0a  49492  elfvne0  49505  lanrcl  50277  ranrcl  50278  rellan  50279  relran  50280  aacllem  50457  amgmw2d  50460