Theorem n0i 4303

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 4301	. . 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 4296

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 3917  df-nul 4297

This theorem is referenced by:  ne0i  4304  n0ii  4306  oprcl  4863  disjss3  5106  elfvdm  6895  mptrcl  6977  isomin  7312  ovrcl  7428  elfvov1  7429  elfvov2  7430  oalimcl  8524  omlimcl  8542  nnaordex2  8603  oaabs2  8613  ecexr  8676  elpmi  8819  elmapex  8821  pmresg  8843  pmsspw  8850  ixpssmap2g  8900  ixpssmapg  8901  resixpfo  8909  php3  9173  cantnfp1lem2  9632  cantnflem1  9642  cnfcom2lem  9654  rankxplim2  9833  rankxplim3  9834  cardlim  9925  alephnbtwn  10024  ttukeylem5  10466  r1wunlim  10690  ssnn0fi  13950  ruclem13  16210  ramtub  16983  elbasfv  17185  elbasov  17186  restsspw  17394  homarcl  17990  grpidval  18588  odlem2  19469  efgrelexlema  19679  subcmn  19767  dvdsrval  20270  elocv  21577  pf1rcl  22236  matrcl  22299  0top  22870  ppttop  22894  pptbas  22895  restrcl  23044  ssrest  23063  iscnp2  23126  lmmo  23267  zfbas  23783  rnelfmlem  23839  isfcls  23896  isnghm  24611  iscau2  25177  itg2cnlem1  25662  itgsubstlem  25955  dchrrcl  27151  clwwlknnn  29962  0ringsubrg  33202  ssdifidllem  33427  ssmxidllem  33444  eulerpartlemgvv  34367  indispconn  35221  cvmtop1  35247  cvmtop2  35248  mrsub0  35503  mrsubf  35504  mrsubccat  35505  mrsubcn  35506  mrsubco  35508  mrsubvrs  35509  msubf  35519  mclsrcl  35548  funpartlem  35930  tailfb  36365  nlpineqsn  37396  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  osumcllem4N  39953  pexmidlem1N  39964  lhpbase  39992  mapco2g  42702  wepwsolem  43031  onov0suclim  43263  uneqsn  44014  relpmin  44942  ssfiunibd  45307  hoicvr  46546  0nelsetpreimafv  47391  termchomn0  49473