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

Theorem ne0i 4299
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 4298 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 3023 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3016  c0 4290
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-ne 3017  df-dif 3938  df-nul 4291
This theorem is referenced by:  ne0d  4300  ne0ii  4302  inelcm  4412  rzal  4451  rexn0  4452  2reu4  4464  tpnzd  4709  issn  4757  brne0  5108  ord0eln0  6239  elfvmptrab1  6788  elovmpt3imp  7391  onnmin  7506  f1oweALT  7664  brovpreldm  7775  bropopvvv  7776  frxp  7811  mpoxopxnop0  7872  brovex  7879  oe1m  8161  oa00  8175  oarec  8178  omord  8184  omeulem1  8198  oewordri  8208  oeordsuc  8210  oelim2  8211  nnmord  8248  map0g  8438  ixpn0  8483  unblem1  8759  wofib  8998  canthwdom  9032  inf1  9074  oemapvali  9136  cantnf  9145  epfrs  9162  acnrcl  9457  iunfictbso  9529  dfac5lem2  9539  kmlem6  9570  fin23lem40  9762  isf34lem7  9790  isf34lem6  9791  fin1a2lem7  9817  fin1a2lem13  9823  alephval2  9983  tskpr  10181  inar1  10186  tskuni  10194  tskxp  10198  tskmap  10199  grur1  10231  axgroth3  10242  inaprc  10247  addclpi  10303  indpi  10318  nqerf  10341  genpn0  10414  infrelb  11615  infssuzle  12320  eliooxr  12785  iccssioo2  12799  iccsupr  12820  elfzoel1  13026  elfzoel2  13027  fzon0  13045  fseqsupubi  13336  hashnn0n0nn  13742  pfxn0  14038  r19.2uz  14701  climuni  14899  ruclem11  15583  bezoutlem2  15878  lcmgcdlem  15940  prmreclem6  16247  vdwlem8  16314  ramtcl  16336  fpwipodrs  17764  gsumval2  17886  mgm2nsgrplem1  18023  sgrp2nmndlem1  18028  issubg3  18237  brgici  18350  odlem2  18598  gexlem2  18638  sylow3lem3  18685  abln0  18918  cyggexb  18950  gsumval3  18958  ablfacrp2  19120  ablfac1c  19124  pgpfaclem2  19135  ringn0  19284  subrgugrp  19485  brlmici  19772  01eq0ring  19975  mpllsslem  20145  ltbwe  20183  mpfrcl  20228  ply1plusgfvi  20340  ply1frcl  20411  cramerimplem2  21223  cramerimplem3  21224  cramerimp  21225  clsval2  21588  lmmo  21918  1stcfb  21983  2ndcsep  21997  ptclsg  22153  txindis  22172  hmphi  22315  trfbas2  22381  flimclslem  22522  ustfilxp  22750  prdsmet  22909  prdsbl  23030  tgioo  23333  caun0  23813  ovolctb  24020  mbflimsup  24196  itg1climres  24244  itg2i1fseq2  24286  dvferm1lem  24510  dvferm2lem  24512  dvferm  24514  c1liplem1  24522  dvivthlem1  24534  aalioulem2  24851  birthdaylem1  25457  tgldimor  26216  axlowdimlem13  26668  uvtx01vtx  27107  wlkreslem  27379  wspniunwspnon  27630  usgr2wspthons3  27671  rusgrnumwwlks  27681  rusgrnumwwlk  27682  frgr2wwlkn0  28035  numclwwlk1  28068  numclwlk1lem1  28076  numclwwlk3  28092  numclwwlk5  28095  ubthlem1  28575  eldmne0  30302  drgextlsp  30896  dimval  30901  dimvalfi  30902  rge0scvg  31092  qqhucn  31133  voliune  31388  eulerpartlemt  31529  erdszelem2  32337  dfso3  32848  sltval2  33061  fnemeet1  33612  fnejoin1  33614  tailfb  33623  curfv  34754  ptrecube  34774  poimirlem23  34797  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  ismblfin  34815  ovoliunnfl  34816  voliunnfl  34818  itg2addnc  34828  totbndbnd  34950  prdsbnd  34954  heibor1lem  34970  prtlem100  35877  prter3  35900  ishlat3N  36372  hlsupr2  36405  elpaddri  36820  diaintclN  38076  dibintclN  38185  dihintcl  38362  rencldnfi  39298  neik0imk0p  40266  clsk3nimkb  40270  amgm3d  40433  amgm4d  40434  prmunb2  40523  rzalf  41154  pwfin0  41204  ssuzfz  41497  fsumiunss  41736  limsupvaluz2  41899  supcnvlimsup  41901  jumpncnp  42061  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  stoweidlem11  42177  stoweidlem31  42197  stoweidlem34  42200  stoweidlem59  42225  fourierdlem31  42304  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem64  42336  fourierdlem73  42345  fourierdlem79  42351  qndenserrnbllem  42460  qndenserrn  42465  sge0rnn0  42531  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem4  42761  ovnlecvr2  42773  hspmbllem2  42790  vonioo  42845  vonicc  42848  smflimsuplem1  42975  smflimsuplem2  42976  cznrng  44124  lmodn0  44448  aacllem  44800  amgmw2d  44803
  Copyright terms: Public domain W3C validator