Theorem n0i 4292

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 4291	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
2	1	con2i 139	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1560   ∈ wcel 2142  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3907  df-nul 4286

This theorem is referenced by:  ne0i  4293  n0ii  4295  oprcl  4857  disjss3  5099  elfvdm  6901  mptrcl  6985  isomin  7321  ovrcl  7437  elfvov1  7438  elfvov2  7439  oalimcl  8529  omlimcl  8547  nnaordex2  8609  oaabs2  8619  ecexr  8683  elpmi  8827  elmapex  8829  pmresg  8852  pmsspw  8859  ixpssmap2g  8909  ixpssmapg  8910  resixpfo  8918  php3  9177  cantnfp1lem2  9634  cantnflem1  9644  cnfcom2lem  9656  rankxplim2  9838  rankxplim3  9839  cardlim  9930  alephnbtwn  10027  ttukeylem5  10470  r1wunlim  10695  ssnn0fi  13998  ruclem13  16274  ramtub  17048  elbasfv  17251  elbasov  17252  restsspw  17460  homarcl  18061  grpidval  18695  odlem2  19579  efgrelexlema  19789  subcmn  19877  dvdsrval  20410  elocv  21720  pf1rcl  22412  matrcl  22472  0top  23043  ppttop  23067  pptbas  23068  restrcl  23217  ssrest  23236  iscnp2  23299  lmmo  23440  zfbas  23956  rnelfmlem  24012  isfcls  24069  isnghm  24783  iscau2  25339  itg2cnlem1  25823  itgsubstlem  26110  dchrrcl  27304  clwwlknnn  30235  0ringsubrg  33432  ssdifidllem  33643  ssmxidllem  33661  eulerpartlemgvv  34673  indispconn  35584  cvmtop1  35610  cvmtop2  35611  mrsub0  35866  mrsubf  35867  mrsubccat  35868  mrsubcn  35869  mrsubco  35871  mrsubvrs  35872  msubf  35882  mclsrcl  35911  funpartlem  36292  tailfb  36737  nlpineqsn  37902  atbase  39913  llnbase  40133  lplnbase  40158  lvolbase  40202  osumcllem4N  40583  pexmidlem1N  40594  lhpbase  40622  mapco2g  43295  wepwsolem  43619  onov0suclim  43851  uneqsn  44601  relpmin  45528  ssfiunibd  45888  hoicvr  47122  0nelsetpreimafv  47996  termchomn0  50105