Theorem ne0i 4282

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3893  df-nul 4275

This theorem is referenced by:  ne0d  4283  ne0ii  4285  inelcm  4406  rzalALT  4436  2reu4  4465  tpnzd  4725  issn  4776  brne0  5136  ord0eln0  6373  elfvunirn  6864  elfvmptrab1  6970  elovmpt3imp  7617  onnmin  7745  f1oweALT  7918  brovpreldm  8032  bropopvvv  8033  frxp  8069  mpoxopxnop0  8158  brovex  8165  ord1eln01  8424  ord2eln012  8425  oe1m  8473  oa00  8487  oarec  8490  omord  8496  omeulem1  8510  oewordri  8521  oeordsuc  8523  oelim2  8524  nnmord  8561  map0g  8825  ixpn0  8871  unblem1  9195  wofib  9453  canthwdom  9487  inf1  9534  oemapvali  9596  cantnf  9605  epfrs  9643  acnrcl  9955  iunfictbso  10027  dfac5lem2  10037  kmlem6  10069  fin23lem40  10264  isf34lem7  10292  isf34lem6  10293  fin1a2lem7  10319  fin1a2lem13  10325  alephval2  10486  tskpr  10684  inar1  10689  tskuni  10697  tskxp  10701  tskmap  10702  grur1  10734  axgroth3  10745  inaprc  10750  addclpi  10806  indpi  10821  nqerf  10844  genpn0  10917  infrelb  12132  infssuzle  12872  eliooxr  13348  iccssioo2  13363  iccsupr  13386  elfzoel1  13602  elfzoel2  13603  fzon0  13623  fseqsupubi  13931  hashnn0n0nn  14344  pfxn0  14640  r19.2uz  15305  climuni  15505  ruclem11  16198  bezoutlem2  16500  lcmgcdlem  16566  prmreclem6  16883  vdwlem8  16950  ramtcl  16972  catcone0  17644  fpwipodrs  18497  gsumval2  18645  mgm2nsgrplem1  18880  sgrp2nmndlem1  18885  issubg3  19111  brgici  19237  odlem2  19505  gexlem2  19548  sylow3lem3  19595  abln0  19833  cyggexb  19865  gsumval3  19873  ablfacrp2  20035  ablfac1c  20039  pgpfaclem2  20050  ringn0  20283  brrici  20473  01eq0ringOLD  20499  subrgugrp  20559  brlmici  21056  mpllsslem  21988  ltbwe  22032  mpfrcl  22073  ply1plusgfvi  22215  ply1frcl  22293  cramerimplem2  22659  cramerimplem3  22660  cramerimp  22661  clsval2  23025  lmmo  23355  1stcfb  23420  2ndcsep  23434  ptclsg  23590  txindis  23609  hmphi  23752  trfbas2  23818  flimclslem  23959  ustfilxp  24188  prdsmet  24345  prdsbl  24466  tgioo  24771  caun0  25258  ovolctb  25467  mbflimsup  25643  itg1climres  25691  itg2i1fseq2  25733  dvferm1lem  25961  dvferm2lem  25963  dvferm  25965  c1liplem1  25973  dvivthlem1  25985  aalioulem2  26310  birthdaylem1  26928  ltsval2  27634  nobdaymin  27759  tgldimor  28584  axlowdimlem13  29037  uvtx01vtx  29480  wlkreslem  29751  wspniunwspnon  30006  usgr2wspthons3  30050  rusgrnumwwlks  30060  rusgrnumwwlk  30061  frgr2wwlkn0  30413  numclwwlk1  30446  numclwlk1lem1  30454  numclwwlk3  30470  numclwwlk5  30473  ubthlem1  30956  n0nsnel  32600  eldmne0  32715  drgextlsp  33753  dimval  33760  dimvalfi  33761  zarcls1  34029  rge0scvg  34109  qqhucn  34152  voliune  34389  eulerpartlemt  34531  erdszelem2  35390  dfso3  35918  fnemeet1  36564  fnejoin1  36566  tailfb  36575  ttc0elw  36725  ttc0el  36733  curfv  37935  ptrecube  37955  poimirlem23  37978  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  ismblfin  37996  ovoliunnfl  37997  voliunnfl  37999  itg2addnc  38009  totbndbnd  38124  prdsbnd  38128  heibor1lem  38144  eldisjdmqsim  39152  prtlem100  39319  prter3  39342  ishlat3N  39814  hlsupr2  39847  elpaddri  40262  diaintclN  41518  dibintclN  41627  dihintcl  41804  unitscyglem4  42651  rencldnfi  43267  omlimcl2  43688  oaun3lem1  43820  neik0imk0p  44481  clsk3nimkb  44485  amgm3d  44644  amgm4d  44645  prmunb2  44756  rzalf  45466  pwfin0  45511  ssuzfz  45797  fsumiunss  46023  limsupvaluz2  46184  supcnvlimsup  46186  jumpncnp  46344  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem11  46457  stoweidlem31  46477  stoweidlem34  46480  stoweidlem59  46505  fourierdlem31  46584  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem64  46616  fourierdlem73  46625  fourierdlem79  46631  qndenserrnbllem  46740  qndenserrn  46745  sge0rnn0  46814  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem4  47044  ovnlecvr2  47056  hspmbllem2  47073  vonioo  47128  vonicc  47131  smflimsuplem1  47266  smflimsuplem2  47267  n0nsn2el  47485  clnbgrn0  48320  brgrici  48401  brgrilci  48493  cznrng  48749  lmodn0  48983  inisegn0a  49323  elfvne0  49336  lanrcl  50108  ranrcl  50109  rellan  50110  relran  50111  aacllem  50288  amgmw2d  50291