Theorem ne0i 4188

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

Syntax hints:   → wi 4   ∈ wcel 2050   ≠ wne 2967  ∅c0 4180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-ne 2968  df-dif 3834  df-nul 4181

This theorem is referenced by:  ne0d  4189  ne0ii  4191  inelcm  4298  rzal  4337  rexn0  4338  2reu4  4350  tpnzd  4590  issn  4638  brne0  4980  ord0eln0  6085  elfvdmOLD  6534  elfvmptrab1  6622  elovmpt3imp  7222  onnmin  7336  f1oweALT  7487  brovpreldm  7594  bropopvvv  7595  frxp  7627  mpoxopxnop0  7686  brovex  7693  oe1m  7974  oa00  7988  oarec  7991  omord  7997  omeulem1  8011  oewordri  8021  oeordsuc  8023  oelim2  8024  nnmord  8061  map0g  8249  ixpn0  8293  unblem1  8567  wofib  8806  canthwdom  8840  inf1  8881  oemapvali  8943  cantnf  8952  epfrs  8969  acnrcl  9264  iunfictbso  9336  dfac5lem2  9346  kmlem6  9377  fin23lem40  9573  isf34lem7  9601  isf34lem6  9602  fin1a2lem7  9628  fin1a2lem13  9634  alephval2  9794  tskpr  9992  inar1  9997  tskuni  10005  tskxp  10009  tskmap  10010  grur1  10042  axgroth3  10053  inaprc  10058  addclpi  10114  indpi  10129  nqerf  10152  genpn0  10225  infrelb  11429  infssuzle  12148  eliooxr  12614  iccssioo2  12628  iccsupr  12649  elfzoel1  12855  elfzoel2  12856  fzon0  12874  fseqsupubi  13164  hashnn0n0nn  13568  swrdn0OLD  13823  pfxn0  13871  r19.2uz  14575  climuni  14773  ruclem11  15456  bezoutlem2  15747  lcmgcdlem  15809  prmreclem6  16116  vdwlem8  16183  ramtcl  16205  fpwipodrs  17635  gsumval2  17751  mgm2nsgrplem1  17877  sgrp2nmndlem1  17882  issubg3  18084  brgici  18184  odlem2  18432  gexlem2  18471  sylow3lem3  18518  abln0  18746  cyggexb  18776  gsumval3  18784  ablfacrp2  18942  ablfac1c  18946  pgpfaclem2  18957  ringn0  19079  subrgugrp  19280  brlmici  19566  01eq0ring  19769  mpllsslem  19932  ltbwe  19969  mpfrcl  20014  ply1plusgfvi  20116  ply1frcl  20187  cramerimplem2  21000  cramerimplem3  21001  cramerimp  21002  clsval2  21365  lmmo  21695  1stcfb  21760  2ndcsep  21774  ptclsg  21930  txindis  21949  hmphi  22092  trfbas2  22158  flimclslem  22299  ustfilxp  22527  prdsmet  22686  prdsbl  22807  tgioo  23110  caun0  23590  ovolctb  23797  mbflimsup  23973  itg1climres  24021  itg2i1fseq2  24063  dvferm1lem  24287  dvferm2lem  24289  dvferm  24291  c1liplem1  24299  dvivthlem1  24311  aalioulem2  24628  birthdaylem1  25234  tgldimor  25993  axlowdimlem13  26446  uvtx01vtx  26885  wlkreslem  27158  wlkreslemOLD  27160  wspniunwspnon  27432  usgr2wspthons3  27473  rusgrnumwwlks  27483  rusgrnumwwlksOLD  27484  rusgrnumwwlk  27485  frgr2wwlkn0  27865  numclwwlk1  27912  numclwlk1lem1  27925  numclwwlk3  27945  numclwwlk5  27948  ubthlem1  28428  slmdbn0  30502  drgextlsp  30625  dimval  30630  dimvalfi  30631  rge0scvg  30836  qqhucn  30877  voliune  31133  eulerpartlemt  31274  erdszelem2  32024  dfso3  32470  sltval2  32684  fnemeet1  33235  fnejoin1  33237  tailfb  33246  curfv  34313  ptrecube  34333  poimirlem23  34356  poimirlem31  34364  poimirlem32  34365  mblfinlem2  34371  ismblfin  34374  ovoliunnfl  34375  voliunnfl  34377  itg2addnc  34387  totbndbnd  34509  prdsbnd  34513  heibor1lem  34529  prtlem100  35440  prter3  35463  ishlat3N  35935  hlsupr2  35968  elpaddri  36383  diaintclN  37639  dibintclN  37748  dihintcl  37925  rencldnfi  38814  neik0imk0p  39749  clsk3nimkb  39753  amgm3d  39917  amgm4d  39918  prmunb2  40059  rzalf  40693  pwfin0  40744  mapdm0OLD  40882  ssuzfz  41047  fsumiunss  41288  limsupvaluz2  41451  supcnvlimsup  41453  jumpncnp  41612  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  stoweidlem11  41728  stoweidlem31  41748  stoweidlem34  41751  stoweidlem59  41776  fourierdlem31  41855  fourierdlem42  41866  fourierdlem48  41871  fourierdlem49  41872  fourierdlem64  41887  fourierdlem73  41896  fourierdlem79  41902  qndenserrnbllem  42011  qndenserrn  42016  sge0rnn0  42082  hoidmvlelem1  42309  hoidmvlelem2  42310  hoidmvlelem4  42312  ovnlecvr2  42324  hspmbllem2  42341  vonioo  42396  vonicc  42399  smflimsuplem1  42526  smflimsuplem2  42527  cznrng  43591  lmodn0  43918  aacllem  44270  amgmw2d  44273