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 140	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2142  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3907  df-nul 4286

This theorem is used by:  ne0i  4293  n0ii  4295  oprcl  4863  disjss3  5107  elfvdm  6915  mptrcl  6999  isomin  7335  ovrcl  7453  elfvov1  7454  elfvov2  7455  oalimcl  8543  omlimcl  8561  nnaordex2  8623  oaabs2  8633  ecexr  8697  elpmi  8841  elmapex  8843  pmresg  8866  pmsspw  8873  ixpssmap2g  8923  ixpssmapg  8924  resixpfo  8932  php3  9191  cantnfp1lem2  9646  cantnflem1  9656  cnfcom2lem  9668  rankxplim2  9850  rankxplim3  9851  cardlim  9965  alephnbtwn  10062  ttukeylem5  10503  r1wunlim  10728  ssnn0fi  14028  ruclem13  16304  ramtub  17078  elbasfv  17281  elbasov  17282  restsspw  17490  homarcl  18091  grpidval  18725  odlem2  19615  efgrelexlema  19825  subcmn  19913  dvdsrval  20450  ssdifidllem  21495  elocv  21829  pf1rcl  22520  matrcl  22580  0top  23151  ppttop  23175  pptbas  23176  restrcl  23325  ssrest  23344  iscnp2  23407  lmmo  23548  zfbas  24064  rnelfmlem  24120  isfcls  24177  isnghm  24891  iscau2  25447  itg2cnlem1  25931  itgsubstlem  26218  dchrrcl  27415  clwwlknnn  30395  0ringsubrg  33580  ssmxidllem  33765  eulerpartlemgvv  34775  indispconn  35734  cvmtop1  35760  cvmtop2  35761  mrsub0  36016  mrsubf  36017  mrsubccat  36018  mrsubcn  36019  mrsubco  36021  mrsubvrs  36022  msubf  36032  mclsrcl  36061  funpartlem  36442  tailfb  36916  nlpineqsn  38082  atbase  40091  llnbase  40311  lplnbase  40336  lvolbase  40380  osumcllem4N  40761  pexmidlem1N  40772  lhpbase  40800  mapco2g  43473  wepwsolem  43797  onov0suclim  44029  uneqsn  44779  relpmin  45689  ssfiunibd  46056  hoicvr  47290  0nelsetpreimafv  48167  termchomn0  50290