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

Theorem n0i 4083
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 4082 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2832 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 318 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 136 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1652  wcel 2155  c0 4078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-dif 3734  df-nul 4079
This theorem is referenced by:  ne0i  4084  n0ii  4086  oprcl  4584  disjss3  4807  elfvdm  6406  mptrcl  6477  isomin  6778  ovrcl  6881  oalimcl  7844  omlimcl  7862  oaabs2  7929  ecexr  7951  elpmi  8078  elmapex  8080  pmresg  8087  pmsspw  8094  ixpssmap2g  8141  ixpssmapg  8142  resixpfo  8150  php3  8352  cantnfp1lem2  8790  cantnflem1  8800  cnfcom2lem  8812  rankxplim2  8957  rankxplim3  8958  cardlim  9048  alephnbtwn  9144  ttukeylem5  9587  r1wunlim  9811  ssnn0fi  12991  ruclem13  15254  ramtub  15996  elbasfv  16193  elbasov  16194  restsspw  16359  homarcl  16944  grpidval  17527  odlem2  18223  efgrelexlema  18427  subcmn  18507  dvdsrval  18911  pf1rcl  19985  elocv  20287  matrcl  20493  0top  21066  ppttop  21090  pptbas  21091  restrcl  21240  ssrest  21259  iscnp2  21322  lmmo  21463  zfbas  21978  rnelfmlem  22034  isfcls  22091  isnghm  22805  iscau2  23353  itg2cnlem1  23818  itgsubstlem  24101  dchrrcl  25255  eleenn  26066  clwwlknnn  27243  eulerpartlemgvv  30819  indispconn  31595  cvmtop1  31621  cvmtop2  31622  mrsub0  31792  mrsubf  31793  mrsubccat  31794  mrsubcn  31795  mrsubco  31797  mrsubvrs  31798  msubf  31808  mclsrcl  31837  funpartlem  32424  tailfb  32746  atbase  35177  llnbase  35397  lplnbase  35422  lvolbase  35466  osumcllem4N  35847  pexmidlem1N  35858  lhpbase  35886  mapco2g  37887  wepwsolem  38221  uneqsn  38927  ssfiunibd  40094  hoicvr  41334
  Copyright terms: Public domain W3C validator