Theorem n0i 4268

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-dif 3886  df-nul 4262

This theorem is referenced by:  ne0i  4269  n0ii  4271  oprcl  4830  disjss3  5071  elfvdm  6861  mptrcl  6945  isomin  7281  ovrcl  7397  elfvov1  7398  elfvov2  7399  oalimcl  8485  omlimcl  8503  nnaordex2  8565  oaabs2  8575  ecexr  8638  elpmi  8783  elmapex  8785  pmresg  8808  pmsspw  8815  ixpssmap2g  8865  ixpssmapg  8866  resixpfo  8874  php3  9133  cantnfp1lem2  9591  cantnflem1  9601  cnfcom2lem  9613  rankxplim2  9795  rankxplim3  9796  cardlim  9887  alephnbtwn  9984  ttukeylem5  10426  r1wunlim  10651  ssnn0fi  13938  ruclem13  16200  ramtub  16974  elbasfv  17176  elbasov  17177  restsspw  17385  homarcl  17986  grpidval  18620  odlem2  19505  efgrelexlema  19715  subcmn  19803  dvdsrval  20332  elocv  21643  pf1rcl  22335  matrcl  22395  0top  22966  ppttop  22990  pptbas  22991  restrcl  23140  ssrest  23159  iscnp2  23222  lmmo  23363  zfbas  23879  rnelfmlem  23935  isfcls  23992  isnghm  24706  iscau2  25262  itg2cnlem1  25746  itgsubstlem  26033  dchrrcl  27221  clwwlknnn  30121  0ringsubrg  33332  ssdifidllem  33539  ssmxidllem  33556  eulerpartlemgvv  34560  indispconn  35462  cvmtop1  35488  cvmtop2  35489  mrsub0  35744  mrsubf  35745  mrsubccat  35746  mrsubcn  35747  mrsubco  35749  mrsubvrs  35750  msubf  35760  mclsrcl  35789  funpartlem  36170  tailfb  36605  nlpineqsn  37770  atbase  39781  llnbase  40001  lplnbase  40026  lvolbase  40070  osumcllem4N  40451  pexmidlem1N  40462  lhpbase  40490  mapco2g  43163  wepwsolem  43487  onov0suclim  43719  uneqsn  44469  relpmin  45396  ssfiunibd  45757  hoicvr  46991  0nelsetpreimafv  47865  termchomn0  49974