Theorem n0i 4301

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-nul 4295

This theorem is referenced by:  ne0i  4302  n0ii  4304  oprcl  4868  disjss3  5112  elfvdm  6916  mptrcl  7000  isomin  7336  ovrcl  7452  elfvov1  7453  elfvov2  7454  oalimcl  8544  omlimcl  8562  nnaordex2  8624  oaabs2  8634  ecexr  8698  elpmi  8842  elmapex  8844  pmresg  8867  pmsspw  8874  ixpssmap2g  8924  ixpssmapg  8925  resixpfo  8933  php3  9192  cantnfp1lem2  9647  cantnflem1  9657  cnfcom2lem  9669  rankxplim2  9851  rankxplim3  9852  cardlim  9957  alephnbtwn  10054  ttukeylem5  10496  r1wunlim  10721  ssnn0fi  14020  ruclem13  16297  ramtub  17071  elbasfv  17274  elbasov  17275  restsspw  17483  homarcl  18084  grpidval  18718  odlem2  19608  efgrelexlema  19818  subcmn  19906  dvdsrval  20442  ssdifidllem  21452  elocv  21786  pf1rcl  22477  matrcl  22537  0top  23108  ppttop  23132  pptbas  23133  restrcl  23282  ssrest  23301  iscnp2  23364  lmmo  23505  zfbas  24021  rnelfmlem  24077  isfcls  24134  isnghm  24848  iscau2  25404  itg2cnlem1  25888  itgsubstlem  26175  dchrrcl  27369  clwwlknnn  30324  0ringsubrg  33511  ssmxidllem  33700  eulerpartlemgvv  34710  indispconn  35624  cvmtop1  35650  cvmtop2  35651  mrsub0  35906  mrsubf  35907  mrsubccat  35908  mrsubcn  35909  mrsubco  35911  mrsubvrs  35912  msubf  35922  mclsrcl  35951  funpartlem  36332  tailfb  36776  nlpineqsn  37941  atbase  39952  llnbase  40172  lplnbase  40197  lvolbase  40241  osumcllem4N  40622  pexmidlem1N  40633  lhpbase  40661  mapco2g  43336  wepwsolem  43660  onov0suclim  43892  uneqsn  44642  relpmin  45552  ssfiunibd  45919  hoicvr  47153  0nelsetpreimafv  48027  termchomn0  50146