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

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

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 3906  df-nul 4285

This theorem is referenced by:  ne0i  4292  n0ii  4294  oprcl  4850  disjss3  5091  elfvdm  6857  mptrcl  6939  isomin  7274  ovrcl  7390  elfvov1  7391  elfvov2  7392  oalimcl  8478  omlimcl  8496  nnaordex2  8557  oaabs2  8567  ecexr  8630  elpmi  8773  elmapex  8775  pmresg  8797  pmsspw  8804  ixpssmap2g  8854  ixpssmapg  8855  resixpfo  8863  php3  9123  cantnfp1lem2  9575  cantnflem1  9585  cnfcom2lem  9597  rankxplim2  9776  rankxplim3  9777  cardlim  9868  alephnbtwn  9965  ttukeylem5  10407  r1wunlim  10631  ssnn0fi  13892  ruclem13  16151  ramtub  16924  elbasfv  17126  elbasov  17127  restsspw  17335  homarcl  17935  grpidval  18535  odlem2  19418  efgrelexlema  19628  subcmn  19716  dvdsrval  20246  elocv  21575  pf1rcl  22234  matrcl  22297  0top  22868  ppttop  22892  pptbas  22893  restrcl  23042  ssrest  23061  iscnp2  23124  lmmo  23265  zfbas  23781  rnelfmlem  23837  isfcls  23894  isnghm  24609  iscau2  25175  itg2cnlem1  25660  itgsubstlem  25953  dchrrcl  27149  clwwlknnn  29977  0ringsubrg  33191  ssdifidllem  33393  ssmxidllem  33410  eulerpartlemgvv  34344  indispconn  35207  cvmtop1  35233  cvmtop2  35234  mrsub0  35489  mrsubf  35490  mrsubccat  35491  mrsubcn  35492  mrsubco  35494  mrsubvrs  35495  msubf  35505  mclsrcl  35534  funpartlem  35916  tailfb  36351  nlpineqsn  37382  atbase  39268  llnbase  39488  lplnbase  39513  lvolbase  39557  osumcllem4N  39938  pexmidlem1N  39949  lhpbase  39977  mapco2g  42687  wepwsolem  43015  onov0suclim  43247  uneqsn  43998  relpmin  44926  ssfiunibd  45291  hoicvr  46529  0nelsetpreimafv  47374  termchomn0  49469