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

Theorem n0i 3953
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 3952 . . 3 ¬ 𝐵 ∈ ∅
2 eleq2 2719 . . 3 (𝐴 = ∅ → (𝐵𝐴𝐵 ∈ ∅))
31, 2mtbiri 316 . 2 (𝐴 = ∅ → ¬ 𝐵𝐴)
43con2i 134 1 (𝐵𝐴 → ¬ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wcel 2030  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  ne0i  3954  n0ii  3955  oprcl  4459  disjss3  4684  mptrcl  6328  isomin  6627  ovrcl  6726  oalimcl  7685  omlimcl  7703  oaabs2  7770  ecexr  7792  elpmi  7918  elmapex  7920  pmresg  7927  pmsspw  7934  ixpssmap2g  7979  ixpssmapg  7980  resixpfo  7988  php3  8187  cantnfp1lem2  8614  cantnflem1  8624  cnfcom2lem  8636  rankxplim2  8781  rankxplim3  8782  cardlim  8836  alephnbtwn  8932  ttukeylem5  9373  r1wunlim  9597  ssnn0fi  12824  ruclem13  15015  ramtub  15763  elbasfv  15967  elbasov  15968  restsspw  16139  homarcl  16725  grpidval  17307  odlem2  18004  efgrelexlema  18208  subcmn  18288  dvdsrval  18691  pf1rcl  19761  elocv  20060  matrcl  20266  0top  20835  ppttop  20859  pptbas  20860  restrcl  21009  ssrest  21028  iscnp2  21091  lmmo  21232  zfbas  21747  rnelfmlem  21803  isfcls  21860  isnghm  22574  iscau2  23121  itg2cnlem1  23573  itgsubstlem  23856  dchrrcl  25010  eleenn  25821  clwwlknnn  26995  eulerpartlemgvv  30566  indispconn  31342  cvmtop1  31368  cvmtop2  31369  mrsub0  31539  mrsubf  31540  mrsubccat  31541  mrsubcn  31542  mrsubco  31544  mrsubvrs  31545  msubf  31555  mclsrcl  31584  funpartlem  32174  tailfb  32497  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  osumcllem4N  35563  pexmidlem1N  35574  lhpbase  35602  mapco2g  37594  wepwsolem  37929  uneqsn  38638  ssfiunibd  39837  hoicvr  41083
  Copyright terms: Public domain W3C validator