MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ne0i Structured version   Visualization version   GIF version

Theorem ne0i 4253
Description: If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
ne0i (𝐵𝐴𝐴 ≠ ∅)

Proof of Theorem ne0i
StepHypRef Expression
1 n0i 4252 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 2997 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wne 2990  c0 4246
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-dif 3887  df-nul 4247
This theorem is referenced by:  ne0d  4254  ne0ii  4256  inelcm  4375  rzal  4414  rexn0  4415  2reu4  4427  tpnzd  4679  issn  4726  brne0  5083  ord0eln0  6217  elfvmptrab1  6776  elovmpt3imp  7386  onnmin  7502  f1oweALT  7659  brovpreldm  7771  bropopvvv  7772  frxp  7807  mpoxopxnop0  7868  brovex  7875  oe1m  8158  oa00  8172  oarec  8175  omord  8181  omeulem1  8195  oewordri  8205  oeordsuc  8207  oelim2  8208  nnmord  8245  map0g  8435  ixpn0  8481  unblem1  8758  wofib  8997  canthwdom  9031  inf1  9073  oemapvali  9135  cantnf  9144  epfrs  9161  acnrcl  9457  iunfictbso  9529  dfac5lem2  9539  kmlem6  9570  fin23lem40  9766  isf34lem7  9794  isf34lem6  9795  fin1a2lem7  9821  fin1a2lem13  9827  alephval2  9987  tskpr  10185  inar1  10190  tskuni  10198  tskxp  10202  tskmap  10203  grur1  10235  axgroth3  10246  inaprc  10251  addclpi  10307  indpi  10322  nqerf  10345  genpn0  10418  infrelb  11617  infssuzle  12323  eliooxr  12787  iccssioo2  12802  iccsupr  12824  elfzoel1  13035  elfzoel2  13036  fzon0  13054  fseqsupubi  13345  hashnn0n0nn  13752  pfxn0  14043  r19.2uz  14707  climuni  14905  ruclem11  15589  bezoutlem2  15882  lcmgcdlem  15944  prmreclem6  16251  vdwlem8  16318  ramtcl  16340  fpwipodrs  17770  gsumval2  17892  mgm2nsgrplem1  18079  sgrp2nmndlem1  18084  issubg3  18293  brgici  18406  odlem2  18663  gexlem2  18703  sylow3lem3  18750  abln0  18984  cyggexb  19016  gsumval3  19024  ablfacrp2  19186  ablfac1c  19190  pgpfaclem2  19201  ringn0  19353  subrgugrp  19551  brlmici  19838  01eq0ring  20042  mpllsslem  20677  ltbwe  20716  mpfrcl  20761  ply1plusgfvi  20875  ply1frcl  20946  cramerimplem2  21293  cramerimplem3  21294  cramerimp  21295  clsval2  21659  lmmo  21989  1stcfb  22054  2ndcsep  22068  ptclsg  22224  txindis  22243  hmphi  22386  trfbas2  22452  flimclslem  22593  ustfilxp  22822  prdsmet  22981  prdsbl  23102  tgioo  23405  caun0  23889  ovolctb  24098  mbflimsup  24274  itg1climres  24322  itg2i1fseq2  24364  dvferm1lem  24591  dvferm2lem  24593  dvferm  24595  c1liplem1  24603  dvivthlem1  24615  aalioulem2  24933  birthdaylem1  25541  tgldimor  26300  axlowdimlem13  26752  uvtx01vtx  27191  wlkreslem  27463  wspniunwspnon  27713  usgr2wspthons3  27754  rusgrnumwwlks  27764  rusgrnumwwlk  27765  frgr2wwlkn0  28117  numclwwlk1  28150  numclwlk1lem1  28158  numclwwlk3  28174  numclwwlk5  28177  ubthlem1  28657  eldmne0  30391  drgextlsp  31088  dimval  31093  dimvalfi  31094  zarcls1  31226  rge0scvg  31306  qqhucn  31347  voliune  31602  eulerpartlemt  31743  erdszelem2  32553  dfso3  33064  sltval2  33277  fnemeet1  33828  fnejoin1  33830  tailfb  33839  curfv  35036  ptrecube  35056  poimirlem23  35079  poimirlem31  35087  poimirlem32  35088  mblfinlem2  35094  ismblfin  35097  ovoliunnfl  35098  voliunnfl  35100  itg2addnc  35110  totbndbnd  35226  prdsbnd  35230  heibor1lem  35246  prtlem100  36154  prter3  36177  ishlat3N  36649  hlsupr2  36682  elpaddri  37097  diaintclN  38353  dibintclN  38462  dihintcl  38639  rencldnfi  39759  neik0imk0p  40736  clsk3nimkb  40740  amgm3d  40902  amgm4d  40903  prmunb2  41012  rzalf  41643  pwfin0  41693  ssuzfz  41978  fsumiunss  42214  limsupvaluz2  42377  supcnvlimsup  42379  jumpncnp  42537  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  stoweidlem11  42650  stoweidlem31  42670  stoweidlem34  42673  stoweidlem59  42698  fourierdlem31  42777  fourierdlem42  42788  fourierdlem48  42793  fourierdlem49  42794  fourierdlem64  42809  fourierdlem73  42818  fourierdlem79  42824  qndenserrnbllem  42933  qndenserrn  42938  sge0rnn0  43004  hoidmvlelem1  43231  hoidmvlelem2  43232  hoidmvlelem4  43234  ovnlecvr2  43246  hspmbllem2  43263  vonioo  43318  vonicc  43321  smflimsuplem1  43448  smflimsuplem2  43449  cznrng  44576  lmodn0  44901  aacllem  45326  amgmw2d  45329
  Copyright terms: Public domain W3C validator