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

Theorem n0i 4068
Description: If a set 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 4067 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2839 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 316 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 136 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wcel 2145  c0 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-nul 4064
This theorem is referenced by:  ne0i  4069  n0ii  4070  oprcl  4565  disjss3  4785  mptrcl  6429  isomin  6728  ovrcl  6829  oalimcl  7792  omlimcl  7810  oaabs2  7877  ecexr  7899  elpmi  8026  elmapex  8028  pmresg  8035  pmsspw  8042  ixpssmap2g  8089  ixpssmapg  8090  resixpfo  8098  php3  8300  cantnfp1lem2  8738  cantnflem1  8748  cnfcom2lem  8760  rankxplim2  8905  rankxplim3  8906  cardlim  8996  alephnbtwn  9092  ttukeylem5  9535  r1wunlim  9759  ssnn0fi  12985  ruclem13  15170  ramtub  15916  elbasfv  16120  elbasov  16121  restsspw  16293  homarcl  16878  grpidval  17461  odlem2  18158  efgrelexlema  18362  subcmn  18442  dvdsrval  18846  pf1rcl  19921  elocv  20222  matrcl  20428  0top  21001  ppttop  21025  pptbas  21026  restrcl  21175  ssrest  21194  iscnp2  21257  lmmo  21398  zfbas  21913  rnelfmlem  21969  isfcls  22026  isnghm  22740  iscau2  23287  itg2cnlem1  23741  itgsubstlem  24024  dchrrcl  25179  eleenn  25990  clwwlknnn  27181  eulerpartlemgvv  30771  indispconn  31547  cvmtop1  31573  cvmtop2  31574  mrsub0  31744  mrsubf  31745  mrsubccat  31746  mrsubcn  31747  mrsubco  31749  mrsubvrs  31750  msubf  31760  mclsrcl  31789  funpartlem  32379  tailfb  32702  atbase  35091  llnbase  35310  lplnbase  35335  lvolbase  35379  osumcllem4N  35760  pexmidlem1N  35771  lhpbase  35799  mapco2g  37796  wepwsolem  38131  uneqsn  38840  ssfiunibd  40033  hoicvr  41275
  Copyright terms: Public domain W3C validator