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  17970  grpidval  18570  odlem2  19453  efgrelexlema  19663  subcmn  19751  dvdsrval  20281  elocv  21610  pf1rcl  22269  matrcl  22332  0top  22903  ppttop  22927  pptbas  22928  restrcl  23077  ssrest  23096  iscnp2  23159  lmmo  23300  zfbas  23816  rnelfmlem  23872  isfcls  23929  isnghm  24644  iscau2  25210  itg2cnlem1  25695  itgsubstlem  25988  dchrrcl  27184  clwwlknnn  30012  0ringsubrg  33218  ssdifidllem  33420  ssmxidllem  33437  eulerpartlemgvv  34360  indispconn  35214  cvmtop1  35240  cvmtop2  35241  mrsub0  35496  mrsubf  35497  mrsubccat  35498  mrsubcn  35499  mrsubco  35501  mrsubvrs  35502  msubf  35512  mclsrcl  35541  funpartlem  35923  tailfb  36358  nlpineqsn  37389  atbase  39275  llnbase  39496  lplnbase  39521  lvolbase  39565  osumcllem4N  39946  pexmidlem1N  39957  lhpbase  39985  mapco2g  42695  wepwsolem  43024  onov0suclim  43256  uneqsn  44007  relpmin  44935  ssfiunibd  45300  hoicvr  46539  0nelsetpreimafv  47384  termchomn0  49466