Theorem n0i 4299

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 4297	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2817	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 327	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 139	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∅c0 4292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3914  df-nul 4293

This theorem is referenced by:  ne0i  4300  n0ii  4302  oprcl  4859  disjss3  5101  elfvdm  6877  mptrcl  6959  isomin  7294  ovrcl  7410  elfvov1  7411  elfvov2  7412  oalimcl  8501  omlimcl  8519  nnaordex2  8580  oaabs2  8590  ecexr  8653  elpmi  8796  elmapex  8798  pmresg  8820  pmsspw  8827  ixpssmap2g  8877  ixpssmapg  8878  resixpfo  8886  php3  9150  cantnfp1lem2  9608  cantnflem1  9618  cnfcom2lem  9630  rankxplim2  9809  rankxplim3  9810  cardlim  9901  alephnbtwn  10000  ttukeylem5  10442  r1wunlim  10666  ssnn0fi  13926  ruclem13  16186  ramtub  16959  elbasfv  17161  elbasov  17162  restsspw  17370  homarcl  17966  grpidval  18564  odlem2  19445  efgrelexlema  19655  subcmn  19743  dvdsrval  20246  elocv  21553  pf1rcl  22212  matrcl  22275  0top  22846  ppttop  22870  pptbas  22871  restrcl  23020  ssrest  23039  iscnp2  23102  lmmo  23243  zfbas  23759  rnelfmlem  23815  isfcls  23872  isnghm  24587  iscau2  25153  itg2cnlem1  25638  itgsubstlem  25931  dchrrcl  27127  clwwlknnn  29935  0ringsubrg  33175  ssdifidllem  33400  ssmxidllem  33417  eulerpartlemgvv  34340  indispconn  35194  cvmtop1  35220  cvmtop2  35221  mrsub0  35476  mrsubf  35477  mrsubccat  35478  mrsubcn  35479  mrsubco  35481  mrsubvrs  35482  msubf  35492  mclsrcl  35521  funpartlem  35903  tailfb  36338  nlpineqsn  37369  atbase  39255  llnbase  39476  lplnbase  39501  lvolbase  39545  osumcllem4N  39926  pexmidlem1N  39937  lhpbase  39965  mapco2g  42675  wepwsolem  43004  onov0suclim  43236  uneqsn  43987  relpmin  44915  ssfiunibd  45280  hoicvr  46519  0nelsetpreimafv  47364  termchomn0  49446