Theorem n0i 4285

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 4046  df-nul 4278

This theorem is used by:  ne0i  4286  n0ii  4288  oprcl  4856  disjss3  5101  elfvdm  6924  mptrcl  7008  isomin  7349  ovrcl  7465  elfvov1  7466  elfvov2  7467  oalimcl  8576  omlimcl  8594  nnaordex2  8656  oaabs2  8666  ecexr  8730  elpmi  8874  elmapex  8876  pmresg  8906  pmsspw  8913  ixpssmap2g  8963  ixpssmapg  8964  resixpfo  8972  php3  9232  cantnfp1lem2  9687  cantnflem1  9697  cnfcom2lem  9709  rankxplim2  9904  rankxplim3  9905  cardlim  10060  alephnbtwn  10157  ttukeylem5  10598  r1wunlim  10829  ssnn0fi  14135  ruclem13  16419  ramtub  17199  elbasfv  17402  elbasov  17403  restsspw  17611  homarcl  18212  grpidval  18849  odlem2  19762  efgrelexlema  19972  subcmn  20060  dvdsrval  20600  ssdifidllem  21649  elocv  21983  pf1rcl  22676  matrcl  22736  0top  23310  ppttop  23334  pptbas  23335  restrcl  23484  ssrest  23503  iscnp2  23566  lmmo  23707  zfbas  24224  rnelfmlem  24280  isfcls  24337  isnghm  25051  iscau2  25607  itg2cnlem1  26091  itgsubstlem  26377  dchrrcl  27576  clwwlknnn  30633  0ringsubrg  33862  ssmxidllem  34048  eulerpartlemgvv  35058  erscottd  35819  indispconn  36117  cvmtop1  36143  cvmtop2  36144  mrsub0  36399  mrsubf  36400  mrsubccat  36401  mrsubcn  36402  mrsubco  36404  mrsubvrs  36405  msubf  36415  mclsrcl  36444  funpartlem  36830  tailfb  37289  nlpineqsn  38468  atbase  40483  llnbase  40703  lplnbase  40728  lvolbase  40772  osumcllem4N  41153  pexmidlem1N  41164  lhpbase  41192  mapco2g  43862  wepwsolem  44186  onov0suclim  44413  uneqsn  45162  relpmin  46078  ssfiunibd  46461  hoicvr  47694  0nelsetpreimafv  48608  termchomn0  50755