Theorem n0i 4334

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-dif 3952  df-nul 4324

This theorem is referenced by:  ne0i  4335  n0ii  4337  oprcl  4900  disjss3  5148  elfvdm  6929  mptrcl  7008  isomin  7334  ovrcl  7450  oalimcl  8560  omlimcl  8578  oaabs2  8648  ecexr  8708  elpmi  8840  elmapex  8842  pmresg  8864  pmsspw  8871  ixpssmap2g  8921  ixpssmapg  8922  resixpfo  8930  php3  9212  php3OLD  9224  cantnfp1lem2  9674  cantnflem1  9684  cnfcom2lem  9696  rankxplim2  9875  rankxplim3  9876  cardlim  9967  alephnbtwn  10066  ttukeylem5  10508  r1wunlim  10732  ssnn0fi  13950  ruclem13  16185  ramtub  16945  elbasfv  17150  elbasov  17151  restsspw  17377  homarcl  17978  grpidval  18580  odlem2  19407  efgrelexlema  19617  subcmn  19705  dvdsrval  20175  elocv  21221  pf1rcl  21868  matrcl  21912  0top  22486  ppttop  22510  pptbas  22511  restrcl  22661  ssrest  22680  iscnp2  22743  lmmo  22884  zfbas  23400  rnelfmlem  23456  isfcls  23513  isnghm  24240  iscau2  24794  itg2cnlem1  25279  itgsubstlem  25565  dchrrcl  26743  clwwlknnn  29286  0ringsubrg  32379  ssmxidllem  32589  eulerpartlemgvv  33375  indispconn  34225  cvmtop1  34251  cvmtop2  34252  mrsub0  34507  mrsubf  34508  mrsubccat  34509  mrsubcn  34510  mrsubco  34512  mrsubvrs  34513  msubf  34523  mclsrcl  34552  funpartlem  34914  tailfb  35262  nlpineqsn  36289  atbase  38159  llnbase  38380  lplnbase  38405  lvolbase  38449  osumcllem4N  38830  pexmidlem1N  38841  lhpbase  38869  mapco2g  41452  wepwsolem  41784  onov0suclim  42024  uneqsn  42776  ssfiunibd  44019  hoicvr  45264  0nelsetpreimafv  46058