Theorem n0i 4286

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

Step	Hyp	Ref	Expression
1		nel02 4285	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
2	1	con2i 140	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-nul 4280

This theorem is used by:  ne0i  4287  n0ii  4289  oprcl  4859  disjss3  5102  elfvdm  6913  mptrcl  6997  isomin  7339  ovrcl  7455  elfvov1  7456  elfvov2  7457  oalimcl  8548  omlimcl  8566  nnaordex2  8628  oaabs2  8638  ecexr  8702  elpmi  8846  elmapex  8848  pmresg  8878  pmsspw  8885  ixpssmap2g  8935  ixpssmapg  8936  resixpfo  8944  php3  9204  cantnfp1lem2  9659  cantnflem1  9669  cnfcom2lem  9681  rankxplim2  9863  rankxplim3  9864  cardlim  9978  alephnbtwn  10075  ttukeylem5  10516  r1wunlim  10747  ssnn0fi  14050  ruclem13  16331  ramtub  17105  elbasfv  17308  elbasov  17309  restsspw  17517  homarcl  18118  grpidval  18755  odlem2  19667  efgrelexlema  19877  subcmn  19965  dvdsrval  20503  ssdifidllem  21548  elocv  21882  pf1rcl  22575  matrcl  22635  0top  23209  ppttop  23233  pptbas  23234  restrcl  23383  ssrest  23402  iscnp2  23465  lmmo  23606  zfbas  24123  rnelfmlem  24179  isfcls  24236  isnghm  24950  iscau2  25506  itg2cnlem1  25990  itgsubstlem  26276  dchrrcl  27477  clwwlknnn  30504  0ringsubrg  33692  ssmxidllem  33877  eulerpartlemgvv  34888  indispconn  35814  cvmtop1  35840  cvmtop2  35841  mrsub0  36096  mrsubf  36097  mrsubccat  36098  mrsubcn  36099  mrsubco  36101  mrsubvrs  36102  msubf  36112  mclsrcl  36141  funpartlem  36522  tailfb  36997  nlpineqsn  38163  atbase  40163  llnbase  40383  lplnbase  40408  lvolbase  40452  osumcllem4N  40833  pexmidlem1N  40844  lhpbase  40872  mapco2g  43560  wepwsolem  43884  onov0suclim  44116  uneqsn  44866  relpmin  45776  ssfiunibd  46143  hoicvr  47377  0nelsetpreimafv  48291  termchomn0  50411