Theorem n0i 4297

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		noel 4294	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2899	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 329	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 141	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1531   ∈ wcel 2108  ∅c0 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-dif 3937  df-nul 4290

This theorem is referenced by:  ne0i  4298  n0ii  4300  oprcl  4821  disjss3  5056  elfvdm  6695  mptrcl  6770  isomin  7082  ovrcl  7189  oalimcl  8178  omlimcl  8196  oaabs2  8264  ecexr  8286  elpmi  8417  elmapex  8419  pmresg  8426  pmsspw  8433  ixpssmap2g  8483  ixpssmapg  8484  resixpfo  8492  php3  8695  cantnfp1lem2  9134  cantnflem1  9144  cnfcom2lem  9156  rankxplim2  9301  rankxplim3  9302  cardlim  9393  alephnbtwn  9489  ttukeylem5  9927  r1wunlim  10151  ssnn0fi  13345  ruclem13  15587  ramtub  16340  elbasfv  16536  elbasov  16537  restsspw  16697  homarcl  17280  grpidval  17863  odlem2  18659  efgrelexlema  18867  subcmn  18949  dvdsrval  19387  pf1rcl  20504  elocv  20804  matrcl  21013  0top  21583  ppttop  21607  pptbas  21608  restrcl  21757  ssrest  21776  iscnp2  21839  lmmo  21980  zfbas  22496  rnelfmlem  22552  isfcls  22609  isnghm  23324  iscau2  23872  itg2cnlem1  24354  itgsubstlem  24637  dchrrcl  25808  clwwlknnn  27803  ssmxidllem  30971  eulerpartlemgvv  31627  indispconn  32474  cvmtop1  32500  cvmtop2  32501  mrsub0  32756  mrsubf  32757  mrsubccat  32758  mrsubcn  32759  mrsubco  32761  mrsubvrs  32762  msubf  32772  mclsrcl  32801  funpartlem  33396  tailfb  33718  nlpineqsn  34681  atbase  36417  llnbase  36637  lplnbase  36662  lvolbase  36706  osumcllem4N  37087  pexmidlem1N  37098  lhpbase  37126  mapco2g  39301  wepwsolem  39632  uneqsn  40363  ssfiunibd  41565  hoicvr  42820  0nelsetpreimafv  43540