Theorem n0i 4291

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-dif 3902  df-nul 4285

This theorem is referenced by:  ne0i  4292  n0ii  4294  oprcl  4852  disjss3  5094  elfvdm  6865  mptrcl  6947  isomin  7280  ovrcl  7396  elfvov1  7397  elfvov2  7398  oalimcl  8484  omlimcl  8502  nnaordex2  8563  oaabs2  8573  ecexr  8636  elpmi  8779  elmapex  8781  pmresg  8803  pmsspw  8810  ixpssmap2g  8860  ixpssmapg  8861  resixpfo  8869  php3  9128  cantnfp1lem2  9579  cantnflem1  9589  cnfcom2lem  9601  rankxplim2  9783  rankxplim3  9784  cardlim  9875  alephnbtwn  9972  ttukeylem5  10414  r1wunlim  10638  ssnn0fi  13902  ruclem13  16161  ramtub  16934  elbasfv  17136  elbasov  17137  restsspw  17345  homarcl  17945  grpidval  18579  odlem2  19461  efgrelexlema  19671  subcmn  19759  dvdsrval  20289  elocv  21615  pf1rcl  22274  matrcl  22337  0top  22908  ppttop  22932  pptbas  22933  restrcl  23082  ssrest  23101  iscnp2  23164  lmmo  23305  zfbas  23821  rnelfmlem  23877  isfcls  23934  isnghm  24648  iscau2  25214  itg2cnlem1  25699  itgsubstlem  25992  dchrrcl  27188  clwwlknnn  30024  0ringsubrg  33229  ssdifidllem  33432  ssmxidllem  33449  eulerpartlemgvv  34400  indispconn  35289  cvmtop1  35315  cvmtop2  35316  mrsub0  35571  mrsubf  35572  mrsubccat  35573  mrsubcn  35574  mrsubco  35576  mrsubvrs  35577  msubf  35587  mclsrcl  35616  funpartlem  35997  tailfb  36432  nlpineqsn  37463  atbase  39398  llnbase  39618  lplnbase  39643  lvolbase  39687  osumcllem4N  40068  pexmidlem1N  40079  lhpbase  40107  mapco2g  42821  wepwsolem  43149  onov0suclim  43381  uneqsn  44132  relpmin  45059  ssfiunibd  45424  hoicvr  46660  0nelsetpreimafv  47504  termchomn0  49599