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

Theorem ne0i 4116
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 4115 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neqned 2981 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wne 2974  c0 4110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-v 3389  df-dif 3766  df-nul 4111
This theorem is referenced by:  ne0d  4117  ne0ii  4119  inelcm  4223  rzal  4262  rexn0  4263  tpnzd  4497  issn  4545  brne0  4887  ord0eln0  5986  elfvdm  6434  elfvmptrab1  6520  elovmpt3imp  7114  onnmin  7227  f1oweALT  7376  brovpreldm  7482  bropopvvv  7483  frxp  7515  mpt2xopxnop0  7570  brovex  7577  oe1m  7856  oa00  7870  oarec  7873  omord  7879  oewordri  7903  oeordsuc  7905  oelim2  7906  nnmord  7943  map0g  8127  ixpn0  8171  unblem1  8445  wofib  8683  canthwdom  8717  inf1  8760  oemapvali  8822  cantnf  8831  epfrs  8848  acnrcl  9142  iunfictbso  9214  dfac5lem2  9224  kmlem6  9256  fin23lem40  9452  isf34lem7  9480  isf34lem6  9481  fin1a2lem7  9507  fin1a2lem13  9513  alephval2  9673  tskpr  9871  inar1  9876  tskuni  9884  tskxp  9888  tskmap  9889  grur1  9921  axgroth3  9932  inaprc  9937  addclpi  9993  indpi  10008  nqerf  10031  genpn0  10104  infrelb  11287  infssuzle  11984  eliooxr  12444  iccssioo2  12458  iccsupr  12479  elfzoel1  12686  elfzoel2  12687  fzon0  12705  fseqsupubi  12995  hashnn0n0nn  13392  swrdn0  13648  r19.2uz  14308  climuni  14500  ruclem11  15183  bezoutlem2  15470  lcmgcdlem  15532  prmreclem6  15836  vdwlem8  15903  ramtcl  15925  fpwipodrs  17363  gsumval2  17479  mgm2nsgrplem1  17604  sgrp2nmndlem1  17609  issubg3  17808  brgici  17908  odlem2  18153  gexlem2  18192  sylow3lem3  18239  abln0  18465  cyggexb  18495  gsumval3  18503  ablfacrp2  18662  ablfac1c  18666  pgpfaclem2  18677  ringn0  18799  subrgugrp  18997  brlmici  19270  01eq0ring  19475  mpllsslem  19638  ltbwe  19675  mpfrcl  19720  ply1plusgfvi  19814  ply1frcl  19885  cramerimplem2  20697  cramerimplem3  20698  cramerimp  20699  clsval2  21062  lmmo  21392  1stcfb  21456  2ndcsep  21470  ptclsg  21626  txindis  21645  hmphi  21788  trfbas2  21854  flimclslem  21995  ustfilxp  22223  prdsmet  22382  prdsbl  22503  tgioo  22806  caun0  23285  ovolctb  23465  mbflimsup  23641  itg1climres  23689  itg2i1fseq2  23731  dvferm1lem  23955  dvferm2lem  23957  dvferm  23959  c1liplem1  23967  dvivthlem1  23979  aalioulem2  24296  pilem3OLD  24416  birthdaylem1  24886  tgldimor  25605  axlowdimlem13  26042  uvtx01vtx  26512  uvtxa01vtx0OLD  26514  wlkreslem  26788  wspniunwspnon  27057  usgr2wspthons3  27100  rusgrnumwwlks  27110  rusgrnumwwlk  27111  frgr2wwlkn0  27497  numclwwlk1  27535  numclwlk1lem1  27543  numclwwlk3  27567  numclwwlk5  27570  ubthlem1  28048  slmdbn0  30080  rge0scvg  30314  qqhucn  30355  voliune  30611  eulerpartlemt  30752  erdszelem2  31491  dfso3  31917  sltval2  32124  fnemeet1  32676  fnejoin1  32678  tailfb  32687  curfv  33696  ptrecube  33716  poimirlem23  33739  poimirlem31  33747  poimirlem32  33748  mblfinlem2  33754  ismblfin  33757  ovoliunnfl  33758  voliunnfl  33760  itg2addnc  33770  totbndbnd  33893  prdsbnd  33897  heibor1lem  33913  prtlem100  34632  prter3  34655  ishlat3N  35128  hlsupr2  35161  elpaddri  35576  diaintclN  36833  dibintclN  36942  dihintcl  37119  rencldnfi  37881  neik0imk0p  38828  clsk3nimkb  38832  amgm3d  38996  amgm4d  38997  prmunb2  39004  rzalf  39664  pwfin0  39718  mapdm0OLD  39866  ssuzfz  40039  fsumiunss  40281  limsupvaluz2  40444  supcnvlimsup  40446  jumpncnp  40585  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  stoweidlem11  40701  stoweidlem31  40721  stoweidlem34  40724  stoweidlem59  40749  fourierdlem31  40828  fourierdlem42  40839  fourierdlem48  40844  fourierdlem49  40845  fourierdlem64  40860  fourierdlem73  40869  fourierdlem79  40875  qndenserrnbllem  40987  qndenserrn  40992  sge0rnn0  41058  hoidmvlelem1  41285  hoidmvlelem2  41286  hoidmvlelem4  41288  ovnlecvr2  41300  hspmbllem2  41317  vonioo  41372  vonicc  41375  smflimsuplem1  41502  smflimsuplem2  41503  2reu4  41696  cznrng  42517  lmodn0  42846  aacllem  43112  amgmw2d  43115
  Copyright terms: Public domain W3C validator