Theorem ne0i 4295

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

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3909  df-nul 4288

This theorem is referenced by:  ne0d  4296  ne0ii  4298  inelcm  4426  rzalALT  4457  2reu4  4486  tpnzd  4747  issn  4798  brne0  5162  ord0eln0  6419  elfvunirn  6913  elfvmptrab1  7020  elovmpt3imp  7669  onnmin  7798  f1oweALT  7970  brovpreldm  8085  bropopvvv  8086  frxp  8123  mpoxopxnop0  8212  brovex  8219  ord1eln01  8482  ord2eln012  8483  oe1m  8531  oa00  8545  oarec  8548  omord  8554  omeulem1  8568  oewordri  8579  oeordsuc  8581  oelim2  8582  nnmord  8619  map0g  8883  ixpn0  8929  unblem1  9253  wofib  9508  canthwdom  9542  inf1  9592  oemapvali  9654  cantnf  9663  epfrs  9701  acnrcl  10027  iunfictbso  10099  dfac5lem2  10109  kmlem6  10140  fin23lem40  10336  isf34lem7  10364  isf34lem6  10365  fin1a2lem7  10391  fin1a2lem13  10397  alephval2  10558  tskpr  10756  inar1  10761  tskuni  10769  tskxp  10773  tskmap  10774  grur1  10806  axgroth3  10817  inaprc  10822  addclpi  10878  indpi  10893  nqerf  10916  genpn0  10989  infrelb  12201  infssuzle  12956  eliooxr  13432  iccssioo2  13447  iccsupr  13470  elfzoel1  13687  elfzoel2  13688  fzon0  13708  fseqsupubi  14016  hashnn0n0nn  14429  pfxn0  14726  r19.2uz  15405  climuni  15605  ruclem11  16297  bezoutlem2  16599  lcmgcdlem  16665  prmreclem6  16982  vdwlem8  17049  ramtcl  17071  catcone0  17744  fpwipodrs  18597  gsumval2  18745  mgm2nsgrplem1  18981  sgrp2nmndlem1  18986  issubg3  19212  brgici  19342  odlem2  19610  gexlem2  19653  sylow3lem3  19700  abln0  19938  cyggexb  19970  gsumval3  19978  ablfacrp2  20140  ablfac1c  20144  pgpfaclem2  20155  ringn0  20395  brrici  20588  01eq0ringOLD  20616  subrgugrp  20677  brlmici  21171  mpllsslem  22130  ltbwe  22176  mpfrcl  22217  ply1plusgfvi  22382  ply1frcl  22459  cramerimplem2  22822  cramerimplem3  22823  cramerimp  22824  clsval2  23188  lmmo  23518  1stcfb  23583  2ndcsep  23597  ptclsg  23753  txindis  23772  hmphi  23915  trfbas2  23981  flimclslem  24122  ustfilxp  24351  prdsmet  24508  prdsbl  24629  tgioo  24934  caun0  25421  ovolctb  25630  mbflimsup  25806  itg1climres  25854  itg2i1fseq2  25896  dvferm1lem  26124  dvferm2lem  26126  dvferm  26128  c1liplem1  26136  dvivthlem1  26148  aalioulem2  26477  birthdaylem1  27097  ltsval2  27801  nobdaymin  27927  tgldimor  28752  perpin  28986  axlowdimlem13  29285  uvtx01vtx  29728  wlkreslem  29998  wspniunwspnon  30253  usgr2wspthons3  30297  rusgrnumwwlks  30307  rusgrnumwwlk  30308  frgr2wwlkn0  30660  numclwwlk1  30693  numclwlk1lem1  30701  numclwwlk3  30717  numclwwlk5  30720  ubthlem1  31203  n0nsnel  32842  eldmne0  32953  drgextlsp  33965  dimval  33972  dimvalfi  33973  zarcls1  34240  rge0scvg  34320  qqhucn  34363  voliune  34600  eulerpartlemt  34742  dfscott3  35493  erdszelem2  35665  dfso3  36193  fnemeet1  36858  fnejoin1  36860  tailfb  36869  ttc0elw  37019  ttc0el  37027  curfv  38232  ptrecube  38252  poimirlem23  38275  poimirlem31  38283  poimirlem32  38284  mblfinlem2  38290  ismblfin  38293  ovoliunnfl  38294  voliunnfl  38296  itg2addnc  38306  totbndbnd  38421  prdsbnd  38425  heibor1lem  38441  eldisjdmqsim  39447  prtlem100  39614  prter3  39637  ishlat3N  40109  hlsupr2  40142  elpaddri  40557  diaintclN  41813  dibintclN  41922  dihintcl  42099  unitscyglem4  42946  rencldnfi  43531  omlimcl2  43952  oaun3lem1  44084  neik0imk0p  44745  clsk3nimkb  44749  amgm3d  44908  amgm4d  44909  prmunb2  45004  rzalf  45720  pwfin0  45765  ssuzfz  46048  fsumiunss  46274  limsupvaluz2  46435  supcnvlimsup  46437  jumpncnp  46595  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stoweidlem11  46708  stoweidlem31  46728  stoweidlem34  46731  stoweidlem59  46756  fourierdlem31  46835  fourierdlem42  46846  fourierdlem64  46867  fourierdlem73  46876  fourierdlem79  46882  qndenserrnbllem  46991  qndenserrn  46996  sge0rnn0  47065  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem4  47295  ovnlecvr2  47307  hspmbllem2  47324  vonioo  47379  vonicc  47382  smflimsuplem1  47517  smflimsuplem2  47518  n0nsn2el  47745  clnbgrn0  48580  brgrici  48661  brgrilci  48753  cznrng  49009  lmodn0  49258  inisegn0a  49597  elfvne0  49610  lanrcl  50382  ranrcl  50383  rellan  50384  relran  50385  aacllem  50584  amgmw2d  50587