Theorem n0i 4249

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 4247	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2878	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 330	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 141	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3884  df-nul 4244

This theorem is referenced by:  ne0i  4250  n0ii  4252  oprcl  4791  disjss3  5029  elfvdm  6677  mptrcl  6754  isomin  7069  ovrcl  7176  oalimcl  8169  omlimcl  8187  oaabs2  8255  ecexr  8277  elpmi  8408  elmapex  8410  pmresg  8417  pmsspw  8424  ixpssmap2g  8474  ixpssmapg  8475  resixpfo  8483  php3  8687  cantnfp1lem2  9126  cantnflem1  9136  cnfcom2lem  9148  rankxplim2  9293  rankxplim3  9294  cardlim  9385  alephnbtwn  9482  ttukeylem5  9924  r1wunlim  10148  ssnn0fi  13348  ruclem13  15587  ramtub  16338  elbasfv  16536  elbasov  16537  restsspw  16697  homarcl  17280  grpidval  17863  odlem2  18659  efgrelexlema  18867  subcmn  18950  dvdsrval  19391  elocv  20357  pf1rcl  20973  matrcl  21017  0top  21588  ppttop  21612  pptbas  21613  restrcl  21762  ssrest  21781  iscnp2  21844  lmmo  21985  zfbas  22501  rnelfmlem  22557  isfcls  22614  isnghm  23329  iscau2  23881  itg2cnlem1  24365  itgsubstlem  24651  dchrrcl  25824  clwwlknnn  27818  ssmxidllem  31049  eulerpartlemgvv  31744  indispconn  32594  cvmtop1  32620  cvmtop2  32621  mrsub0  32876  mrsubf  32877  mrsubccat  32878  mrsubcn  32879  mrsubco  32881  mrsubvrs  32882  msubf  32892  mclsrcl  32921  funpartlem  33516  tailfb  33838  nlpineqsn  34825  atbase  36585  llnbase  36805  lplnbase  36830  lvolbase  36874  osumcllem4N  37255  pexmidlem1N  37266  lhpbase  37294  mapco2g  39655  wepwsolem  39986  uneqsn  40726  ssfiunibd  41941  hoicvr  43187  0nelsetpreimafv  43907