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

Theorem n0i 3576
Description: If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
n0i  |-  ( B  e.  A  ->  -.  A  =  (/) )

Proof of Theorem n0i
StepHypRef Expression
1 noel 3575 . . 3  |-  -.  B  e.  (/)
2 eleq2 2448 . . 3  |-  ( A  =  (/)  ->  ( B  e.  A  <->  B  e.  (/) ) )
31, 2mtbiri 295 . 2  |-  ( A  =  (/)  ->  -.  B  e.  A )
43con2i 114 1  |-  ( B  e.  A  ->  -.  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    e. wcel 1717   (/)c0 3571
This theorem is referenced by:  ne0i  3577  oprcl  3950  disjss3  4152  iin0  4314  snsn0non  4640  isomin  5996  ovrcl  6050  tfrlem16  6590  oalimcl  6739  omlimcl  6757  oaabs2  6824  ecexr  6846  elpmi  6971  elmapex  6973  pmresg  6977  pmsspw  6984  ixpssmap2g  7027  ixpssmapg  7028  resixpfo  7036  php3  7229  cantnfp1lem2  7568  cantnflem1  7578  cnfcom2lem  7591  rankxplim2  7737  rankxplim3  7738  cardlim  7792  alephnbtwn  7885  pwcdadom  8029  ttukeylem5  8326  r1wunlim  8545  nnunb  10149  ruclem13  12768  ramtub  13307  elbasfv  13439  elbasov  13440  restsspw  13586  homarcl  14110  grpidval  14634  odlem2  15104  efgrelexlema  15308  subcmn  15383  dvdsrval  15677  elocv  16818  0top  16971  ppttop  16994  pptbas  16995  restrcl  17143  ssrest  17162  iscnp2  17225  lmmo  17366  zfbas  17849  rnelfmlem  17905  isfcls  17962  isnghm  18628  iscau2  19101  itg2cnlem1  19520  itgsubstlem  19799  pf1rcl  19836  dchrrcl  20891  nbgranself2  21314  uvtxisvtx  21365  uvtx01vtx  21367  hon0  23144  dmadjrnb  23257  indispcon  24700  cvmtop1  24726  cvmtop2  24727  funpartlem  25505  eleenn  25549  tailfb  26097  mapco2g  26460  wepwsolem  26807  matrcl  27135  bnj98  28576  atbase  29404  llnbase  29623  lplnbase  29648  lvolbase  29692  osumcllem4N  30073  pexmidlem1N  30084  lhpbase  30112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-dif 3266  df-nul 3572
  Copyright terms: Public domain W3C validator