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

Theorem n0i 3896
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 3895 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2687 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 317 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 134 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wcel 1987  c0 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-nul 3892
This theorem is referenced by:  ne0i  3897  n0ii  3898  oprcl  4395  disjss3  4612  mptrcl  6246  isomin  6541  ovrcl  6639  oalimcl  7585  omlimcl  7603  oaabs2  7670  ecexr  7692  elpmi  7820  elmapex  7822  pmresg  7829  pmsspw  7836  ixpssmap2g  7881  ixpssmapg  7882  resixpfo  7890  php3  8090  cantnfp1lem2  8520  cantnflem1  8530  cnfcom2lem  8542  rankxplim2  8687  rankxplim3  8688  cardlim  8742  alephnbtwn  8838  ttukeylem5  9279  r1wunlim  9503  ssnn0fi  12724  ruclem13  14896  ramtub  15640  elbasfv  15841  elbasov  15842  restsspw  16013  homarcl  16599  grpidval  17181  odlem2  17879  efgrelexlema  18083  subcmn  18163  dvdsrval  18566  pf1rcl  19632  elocv  19931  matrcl  20137  0top  20698  ppttop  20721  pptbas  20722  restrcl  20871  ssrest  20890  iscnp2  20953  lmmo  21094  zfbas  21610  rnelfmlem  21666  isfcls  21723  isnghm  22437  iscau2  22983  itg2cnlem1  23434  itgsubstlem  23715  dchrrcl  24865  eleenn  25676  eulerpartlemgvv  30219  indispconn  30924  cvmtop1  30950  cvmtop2  30951  mrsub0  31121  mrsubf  31122  mrsubccat  31123  mrsubcn  31124  mrsubco  31126  mrsubvrs  31127  msubf  31137  mclsrcl  31166  funpartlem  31691  tailfb  32014  atbase  34056  llnbase  34275  lplnbase  34300  lvolbase  34344  osumcllem4N  34725  pexmidlem1N  34736  lhpbase  34764  mapco2g  36757  wepwsolem  37092  uneqsn  37803  ssfiunibd  38987  hoicvr  40069
  Copyright terms: Public domain W3C validator