Theorem n0i 4290

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-dif 3902  df-nul 4284

This theorem is referenced by:  ne0i  4291  n0ii  4293  oprcl  4853  disjss3  5095  elfvdm  6866  mptrcl  6948  isomin  7281  ovrcl  7397  elfvov1  7398  elfvov2  7399  oalimcl  8485  omlimcl  8503  nnaordex2  8565  oaabs2  8575  ecexr  8638  elpmi  8781  elmapex  8783  pmresg  8806  pmsspw  8813  ixpssmap2g  8863  ixpssmapg  8864  resixpfo  8872  php3  9131  cantnfp1lem2  9586  cantnflem1  9596  cnfcom2lem  9608  rankxplim2  9790  rankxplim3  9791  cardlim  9882  alephnbtwn  9979  ttukeylem5  10421  r1wunlim  10646  ssnn0fi  13906  ruclem13  16165  ramtub  16938  elbasfv  17140  elbasov  17141  restsspw  17349  homarcl  17950  grpidval  18584  odlem2  19466  efgrelexlema  19676  subcmn  19764  dvdsrval  20295  elocv  21621  pf1rcl  22291  matrcl  22354  0top  22925  ppttop  22949  pptbas  22950  restrcl  23099  ssrest  23118  iscnp2  23181  lmmo  23322  zfbas  23838  rnelfmlem  23894  isfcls  23951  isnghm  24665  iscau2  25231  itg2cnlem1  25716  itgsubstlem  26009  dchrrcl  27205  clwwlknnn  30057  0ringsubrg  33282  ssdifidllem  33486  ssmxidllem  33503  eulerpartlemgvv  34482  indispconn  35377  cvmtop1  35403  cvmtop2  35404  mrsub0  35659  mrsubf  35660  mrsubccat  35661  mrsubcn  35662  mrsubco  35664  mrsubvrs  35665  msubf  35675  mclsrcl  35704  funpartlem  36085  tailfb  36520  nlpineqsn  37552  atbase  39488  llnbase  39708  lplnbase  39733  lvolbase  39777  osumcllem4N  40158  pexmidlem1N  40169  lhpbase  40197  mapco2g  42898  wepwsolem  43226  onov0suclim  43458  uneqsn  44208  relpmin  45135  ssfiunibd  45499  hoicvr  46734  0nelsetpreimafv  47578  termchomn0  49671