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

Theorem n0i 4297
Description: If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
n0i (𝐵𝐴 → ¬ 𝐴 = ∅)

Proof of Theorem n0i
StepHypRef Expression
1 noel 4294 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2899 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 329 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 141 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wcel 2107  c0 4289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-dif 3937  df-nul 4290
This theorem is referenced by:  ne0i  4298  n0ii  4300  oprcl  4821  disjss3  5056  elfvdm  6695  mptrcl  6770  isomin  7082  ovrcl  7189  oalimcl  8178  omlimcl  8196  oaabs2  8264  ecexr  8286  elpmi  8417  elmapex  8419  pmresg  8426  pmsspw  8433  ixpssmap2g  8483  ixpssmapg  8484  resixpfo  8492  php3  8695  cantnfp1lem2  9134  cantnflem1  9144  cnfcom2lem  9156  rankxplim2  9301  rankxplim3  9302  cardlim  9393  alephnbtwn  9489  ttukeylem5  9927  r1wunlim  10151  ssnn0fi  13345  ruclem13  15587  ramtub  16340  elbasfv  16536  elbasov  16537  restsspw  16697  homarcl  17280  grpidval  17863  odlem2  18659  efgrelexlema  18867  subcmn  18949  dvdsrval  19387  pf1rcl  20504  elocv  20804  matrcl  21013  0top  21583  ppttop  21607  pptbas  21608  restrcl  21757  ssrest  21776  iscnp2  21839  lmmo  21980  zfbas  22496  rnelfmlem  22552  isfcls  22609  isnghm  23324  iscau2  23872  itg2cnlem1  24354  itgsubstlem  24637  dchrrcl  25808  clwwlknnn  27803  eulerpartlemgvv  31622  indispconn  32469  cvmtop1  32495  cvmtop2  32496  mrsub0  32751  mrsubf  32752  mrsubccat  32753  mrsubcn  32754  mrsubco  32756  mrsubvrs  32757  msubf  32767  mclsrcl  32796  funpartlem  33391  tailfb  33713  nlpineqsn  34671  atbase  36407  llnbase  36627  lplnbase  36652  lvolbase  36696  osumcllem4N  37077  pexmidlem1N  37088  lhpbase  37116  mapco2g  39291  wepwsolem  39622  uneqsn  40353  ssfiunibd  41555  hoicvr  42810  0nelsetpreimafv  43530
  Copyright terms: Public domain W3C validator