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

Theorem ne0i 4297
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 4296 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 3020 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3013  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ne 3014  df-dif 3936  df-nul 4289
This theorem is referenced by:  ne0d  4298  ne0ii  4300  inelcm  4410  rzal  4449  rexn0  4450  2reu4  4462  tpnzd  4707  issn  4755  brne0  5107  ord0eln0  6238  elfvmptrab1  6787  elovmpt3imp  7391  onnmin  7507  f1oweALT  7662  brovpreldm  7773  bropopvvv  7774  frxp  7809  mpoxopxnop0  7870  brovex  7877  oe1m  8160  oa00  8174  oarec  8177  omord  8183  omeulem1  8197  oewordri  8207  oeordsuc  8209  oelim2  8210  nnmord  8247  map0g  8437  ixpn0  8482  unblem1  8758  wofib  8997  canthwdom  9031  inf1  9073  oemapvali  9135  cantnf  9144  epfrs  9161  acnrcl  9456  iunfictbso  9528  dfac5lem2  9538  kmlem6  9569  fin23lem40  9761  isf34lem7  9789  isf34lem6  9790  fin1a2lem7  9816  fin1a2lem13  9822  alephval2  9982  tskpr  10180  inar1  10185  tskuni  10193  tskxp  10197  tskmap  10198  grur1  10230  axgroth3  10241  inaprc  10246  addclpi  10302  indpi  10317  nqerf  10340  genpn0  10413  infrelb  11614  infssuzle  12319  eliooxr  12783  iccssioo2  12797  iccsupr  12818  elfzoel1  13024  elfzoel2  13025  fzon0  13043  fseqsupubi  13334  hashnn0n0nn  13740  pfxn0  14036  r19.2uz  14699  climuni  14897  ruclem11  15581  bezoutlem2  15876  lcmgcdlem  15938  prmreclem6  16245  vdwlem8  16312  ramtcl  16334  fpwipodrs  17762  gsumval2  17884  mgm2nsgrplem1  18021  sgrp2nmndlem1  18026  issubg3  18235  brgici  18348  odlem2  18596  gexlem2  18636  sylow3lem3  18683  abln0  18916  cyggexb  18948  gsumval3  18956  ablfacrp2  19118  ablfac1c  19122  pgpfaclem2  19133  ringn0  19282  subrgugrp  19483  brlmici  19770  01eq0ring  19973  mpllsslem  20143  ltbwe  20181  mpfrcl  20226  ply1plusgfvi  20338  ply1frcl  20409  cramerimplem2  21221  cramerimplem3  21222  cramerimp  21223  clsval2  21586  lmmo  21916  1stcfb  21981  2ndcsep  21995  ptclsg  22151  txindis  22170  hmphi  22313  trfbas2  22379  flimclslem  22520  ustfilxp  22748  prdsmet  22907  prdsbl  23028  tgioo  23331  caun0  23811  ovolctb  24018  mbflimsup  24194  itg1climres  24242  itg2i1fseq2  24284  dvferm1lem  24508  dvferm2lem  24510  dvferm  24512  c1liplem1  24520  dvivthlem1  24532  aalioulem2  24849  birthdaylem1  25456  tgldimor  26215  axlowdimlem13  26667  uvtx01vtx  27106  wlkreslem  27378  wspniunwspnon  27629  usgr2wspthons3  27670  rusgrnumwwlks  27680  rusgrnumwwlk  27681  frgr2wwlkn0  28034  numclwwlk1  28067  numclwlk1lem1  28075  numclwwlk3  28091  numclwwlk5  28094  ubthlem1  28574  eldmne0  30301  drgextlsp  30895  dimval  30900  dimvalfi  30901  rge0scvg  31091  qqhucn  31132  voliune  31387  eulerpartlemt  31528  erdszelem2  32336  dfso3  32847  sltval2  33060  fnemeet1  33611  fnejoin1  33613  tailfb  33622  curfv  34753  ptrecube  34773  poimirlem23  34796  poimirlem31  34804  poimirlem32  34805  mblfinlem2  34811  ismblfin  34814  ovoliunnfl  34815  voliunnfl  34817  itg2addnc  34827  totbndbnd  34948  prdsbnd  34952  heibor1lem  34968  prtlem100  35875  prter3  35898  ishlat3N  36370  hlsupr2  36403  elpaddri  36818  diaintclN  38074  dibintclN  38183  dihintcl  38360  rencldnfi  39296  neik0imk0p  40264  clsk3nimkb  40268  amgm3d  40430  amgm4d  40431  prmunb2  40520  rzalf  41151  pwfin0  41201  ssuzfz  41493  fsumiunss  41732  limsupvaluz2  41895  supcnvlimsup  41897  jumpncnp  42057  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stoweidlem11  42173  stoweidlem31  42193  stoweidlem34  42196  stoweidlem59  42221  fourierdlem31  42300  fourierdlem42  42311  fourierdlem48  42316  fourierdlem49  42317  fourierdlem64  42332  fourierdlem73  42341  fourierdlem79  42347  qndenserrnbllem  42456  qndenserrn  42461  sge0rnn0  42527  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem4  42757  ovnlecvr2  42769  hspmbllem2  42786  vonioo  42841  vonicc  42844  smflimsuplem1  42971  smflimsuplem2  42972  cznrng  44154  lmodn0  44478  aacllem  44830  amgmw2d  44833
  Copyright terms: Public domain W3C validator