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

Theorem n0i 4298
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 4295 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2827 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 327 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 139 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2107  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-dif 3918  df-nul 4288
This theorem is referenced by:  ne0i  4299  n0ii  4301  oprcl  4861  disjss3  5109  elfvdm  6884  mptrcl  6962  isomin  7287  ovrcl  7403  oalimcl  8512  omlimcl  8530  oaabs2  8600  ecexr  8660  elpmi  8791  elmapex  8793  pmresg  8815  pmsspw  8822  ixpssmap2g  8872  ixpssmapg  8873  resixpfo  8881  php3  9163  php3OLD  9175  cantnfp1lem2  9622  cantnflem1  9632  cnfcom2lem  9644  rankxplim2  9823  rankxplim3  9824  cardlim  9915  alephnbtwn  10014  ttukeylem5  10456  r1wunlim  10680  ssnn0fi  13897  ruclem13  16131  ramtub  16891  elbasfv  17096  elbasov  17097  restsspw  17320  homarcl  17921  grpidval  18523  odlem2  19328  efgrelexlema  19538  subcmn  19622  dvdsrval  20081  elocv  21088  pf1rcl  21731  matrcl  21775  0top  22349  ppttop  22373  pptbas  22374  restrcl  22524  ssrest  22543  iscnp2  22606  lmmo  22747  zfbas  23263  rnelfmlem  23319  isfcls  23376  isnghm  24103  iscau2  24657  itg2cnlem1  25142  itgsubstlem  25428  dchrrcl  26604  clwwlknnn  29019  0ringsubrg  32106  ssmxidllem  32278  eulerpartlemgvv  33016  indispconn  33868  cvmtop1  33894  cvmtop2  33895  mrsub0  34150  mrsubf  34151  mrsubccat  34152  mrsubcn  34153  mrsubco  34155  mrsubvrs  34156  msubf  34166  mclsrcl  34195  funpartlem  34556  tailfb  34878  nlpineqsn  35908  atbase  37780  llnbase  38001  lplnbase  38026  lvolbase  38070  osumcllem4N  38451  pexmidlem1N  38462  lhpbase  38490  mapco2g  41066  wepwsolem  41398  onov0suclim  41638  uneqsn  42371  ssfiunibd  43617  hoicvr  44863  0nelsetpreimafv  45656
  Copyright terms: Public domain W3C validator