Theorem n0i 4267

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2106  ∅c0 4256

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-dif 3890  df-nul 4257

This theorem is referenced by:  ne0i  4268  n0ii  4270  oprcl  4830  disjss3  5073  elfvdm  6806  mptrcl  6884  isomin  7208  ovrcl  7316  oalimcl  8391  omlimcl  8409  oaabs2  8479  ecexr  8503  elpmi  8634  elmapex  8636  pmresg  8658  pmsspw  8665  ixpssmap2g  8715  ixpssmapg  8716  resixpfo  8724  php3  8995  php3OLD  9007  cantnfp1lem2  9437  cantnflem1  9447  cnfcom2lem  9459  rankxplim2  9638  rankxplim3  9639  cardlim  9730  alephnbtwn  9827  ttukeylem5  10269  r1wunlim  10493  ssnn0fi  13705  ruclem13  15951  ramtub  16713  elbasfv  16918  elbasov  16919  restsspw  17142  homarcl  17743  grpidval  18345  odlem2  19147  efgrelexlema  19355  subcmn  19438  dvdsrval  19887  elocv  20873  pf1rcl  21515  matrcl  21559  0top  22133  ppttop  22157  pptbas  22158  restrcl  22308  ssrest  22327  iscnp2  22390  lmmo  22531  zfbas  23047  rnelfmlem  23103  isfcls  23160  isnghm  23887  iscau2  24441  itg2cnlem1  24926  itgsubstlem  25212  dchrrcl  26388  clwwlknnn  28397  ssmxidllem  31641  eulerpartlemgvv  32343  indispconn  33196  cvmtop1  33222  cvmtop2  33223  mrsub0  33478  mrsubf  33479  mrsubccat  33480  mrsubcn  33481  mrsubco  33483  mrsubvrs  33484  msubf  33494  mclsrcl  33523  funpartlem  34244  tailfb  34566  nlpineqsn  35579  atbase  37303  llnbase  37523  lplnbase  37548  lvolbase  37592  osumcllem4N  37973  pexmidlem1N  37984  lhpbase  38012  mapco2g  40536  wepwsolem  40867  uneqsn  41633  ssfiunibd  42848  hoicvr  44086  0nelsetpreimafv  44842