Theorem n0i 4280

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-nul 4274

This theorem is referenced by:  ne0i  4281  n0ii  4283  oprcl  4842  disjss3  5084  elfvdm  6874  mptrcl  6957  isomin  7292  ovrcl  7408  elfvov1  7409  elfvov2  7410  oalimcl  8495  omlimcl  8513  nnaordex2  8575  oaabs2  8585  ecexr  8648  elpmi  8793  elmapex  8795  pmresg  8818  pmsspw  8825  ixpssmap2g  8875  ixpssmapg  8876  resixpfo  8884  php3  9143  cantnfp1lem2  9600  cantnflem1  9610  cnfcom2lem  9622  rankxplim2  9804  rankxplim3  9805  cardlim  9896  alephnbtwn  9993  ttukeylem5  10435  r1wunlim  10660  ssnn0fi  13947  ruclem13  16209  ramtub  16983  elbasfv  17185  elbasov  17186  restsspw  17394  homarcl  17995  grpidval  18629  odlem2  19514  efgrelexlema  19724  subcmn  19812  dvdsrval  20341  elocv  21648  pf1rcl  22314  matrcl  22377  0top  22948  ppttop  22972  pptbas  22973  restrcl  23122  ssrest  23141  iscnp2  23204  lmmo  23345  zfbas  23861  rnelfmlem  23917  isfcls  23974  isnghm  24688  iscau2  25244  itg2cnlem1  25728  itgsubstlem  26015  dchrrcl  27203  clwwlknnn  30103  0ringsubrg  33312  ssdifidllem  33516  ssmxidllem  33533  eulerpartlemgvv  34520  indispconn  35416  cvmtop1  35442  cvmtop2  35443  mrsub0  35698  mrsubf  35699  mrsubccat  35700  mrsubcn  35701  mrsubco  35703  mrsubvrs  35704  msubf  35714  mclsrcl  35743  funpartlem  36124  tailfb  36559  nlpineqsn  37724  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  osumcllem4N  40405  pexmidlem1N  40416  lhpbase  40444  mapco2g  43146  wepwsolem  43470  onov0suclim  43702  uneqsn  44452  relpmin  45379  ssfiunibd  45742  hoicvr  46976  0nelsetpreimafv  47850  termchomn0  49959