Theorem n0i 4332

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-dif 3950  df-nul 4322

This theorem is referenced by:  ne0i  4333  n0ii  4335  oprcl  4898  disjss3  5146  elfvdm  6925  mptrcl  7004  isomin  7330  ovrcl  7446  oalimcl  8556  omlimcl  8574  oaabs2  8644  ecexr  8704  elpmi  8836  elmapex  8838  pmresg  8860  pmsspw  8867  ixpssmap2g  8917  ixpssmapg  8918  resixpfo  8926  php3  9208  php3OLD  9220  cantnfp1lem2  9670  cantnflem1  9680  cnfcom2lem  9692  rankxplim2  9871  rankxplim3  9872  cardlim  9963  alephnbtwn  10062  ttukeylem5  10504  r1wunlim  10728  ssnn0fi  13946  ruclem13  16181  ramtub  16941  elbasfv  17146  elbasov  17147  restsspw  17373  homarcl  17974  grpidval  18576  odlem2  19401  efgrelexlema  19611  subcmn  19699  dvdsrval  20167  elocv  21212  pf1rcl  21859  matrcl  21903  0top  22477  ppttop  22501  pptbas  22502  restrcl  22652  ssrest  22671  iscnp2  22734  lmmo  22875  zfbas  23391  rnelfmlem  23447  isfcls  23504  isnghm  24231  iscau2  24785  itg2cnlem1  25270  itgsubstlem  25556  dchrrcl  26732  clwwlknnn  29275  0ringsubrg  32366  ssmxidllem  32577  eulerpartlemgvv  33363  indispconn  34213  cvmtop1  34239  cvmtop2  34240  mrsub0  34495  mrsubf  34496  mrsubccat  34497  mrsubcn  34498  mrsubco  34500  mrsubvrs  34501  msubf  34511  mclsrcl  34540  funpartlem  34902  tailfb  35250  nlpineqsn  36277  atbase  38147  llnbase  38368  lplnbase  38393  lvolbase  38437  osumcllem4N  38818  pexmidlem1N  38829  lhpbase  38857  mapco2g  41437  wepwsolem  41769  onov0suclim  42009  uneqsn  42761  ssfiunibd  44005  hoicvr  45250  0nelsetpreimafv  46044