Theorem n0i 4340

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-dif 3954  df-nul 4334

This theorem is referenced by:  ne0i  4341  n0ii  4343  oprcl  4899  disjss3  5142  elfvdm  6943  mptrcl  7025  isomin  7357  ovrcl  7472  elfvov1  7473  elfvov2  7474  oalimcl  8598  omlimcl  8616  nnaordex2  8677  oaabs2  8687  ecexr  8750  elpmi  8886  elmapex  8888  pmresg  8910  pmsspw  8917  ixpssmap2g  8967  ixpssmapg  8968  resixpfo  8976  php3  9249  php3OLD  9261  cantnfp1lem2  9719  cantnflem1  9729  cnfcom2lem  9741  rankxplim2  9920  rankxplim3  9921  cardlim  10012  alephnbtwn  10111  ttukeylem5  10553  r1wunlim  10777  ssnn0fi  14026  ruclem13  16278  ramtub  17050  elbasfv  17253  elbasov  17254  restsspw  17476  homarcl  18073  grpidval  18674  odlem2  19557  efgrelexlema  19767  subcmn  19855  dvdsrval  20361  elocv  21686  pf1rcl  22353  matrcl  22416  0top  22990  ppttop  23014  pptbas  23015  restrcl  23165  ssrest  23184  iscnp2  23247  lmmo  23388  zfbas  23904  rnelfmlem  23960  isfcls  24017  isnghm  24744  iscau2  25311  itg2cnlem1  25796  itgsubstlem  26089  dchrrcl  27284  clwwlknnn  30052  0ringsubrg  33255  ssdifidllem  33484  ssmxidllem  33501  eulerpartlemgvv  34378  indispconn  35239  cvmtop1  35265  cvmtop2  35266  mrsub0  35521  mrsubf  35522  mrsubccat  35523  mrsubcn  35524  mrsubco  35526  mrsubvrs  35527  msubf  35537  mclsrcl  35566  funpartlem  35943  tailfb  36378  nlpineqsn  37409  atbase  39290  llnbase  39511  lplnbase  39536  lvolbase  39580  osumcllem4N  39961  pexmidlem1N  39972  lhpbase  40000  mapco2g  42725  wepwsolem  43054  onov0suclim  43287  uneqsn  44038  relpmin  44973  ssfiunibd  45321  hoicvr  46563  0nelsetpreimafv  47377  termchomn0  49129