Theorem n0i 4287

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-dif 3900  df-nul 4281

This theorem is referenced by:  ne0i  4288  n0ii  4290  oprcl  4848  disjss3  5088  elfvdm  6856  mptrcl  6938  isomin  7271  ovrcl  7387  elfvov1  7388  elfvov2  7389  oalimcl  8475  omlimcl  8493  nnaordex2  8554  oaabs2  8564  ecexr  8627  elpmi  8770  elmapex  8772  pmresg  8794  pmsspw  8801  ixpssmap2g  8851  ixpssmapg  8852  resixpfo  8860  php3  9118  cantnfp1lem2  9569  cantnflem1  9579  cnfcom2lem  9591  rankxplim2  9773  rankxplim3  9774  cardlim  9865  alephnbtwn  9962  ttukeylem5  10404  r1wunlim  10628  ssnn0fi  13892  ruclem13  16151  ramtub  16924  elbasfv  17126  elbasov  17127  restsspw  17335  homarcl  17935  grpidval  18569  odlem2  19451  efgrelexlema  19661  subcmn  19749  dvdsrval  20279  elocv  21605  pf1rcl  22264  matrcl  22327  0top  22898  ppttop  22922  pptbas  22923  restrcl  23072  ssrest  23091  iscnp2  23154  lmmo  23295  zfbas  23811  rnelfmlem  23867  isfcls  23924  isnghm  24638  iscau2  25204  itg2cnlem1  25689  itgsubstlem  25982  dchrrcl  27178  clwwlknnn  30013  0ringsubrg  33218  ssdifidllem  33421  ssmxidllem  33438  eulerpartlemgvv  34389  indispconn  35278  cvmtop1  35304  cvmtop2  35305  mrsub0  35560  mrsubf  35561  mrsubccat  35562  mrsubcn  35563  mrsubco  35565  mrsubvrs  35566  msubf  35576  mclsrcl  35605  funpartlem  35984  tailfb  36419  nlpineqsn  37450  atbase  39336  llnbase  39556  lplnbase  39581  lvolbase  39625  osumcllem4N  40006  pexmidlem1N  40017  lhpbase  40045  mapco2g  42755  wepwsolem  43083  onov0suclim  43315  uneqsn  44066  relpmin  44993  ssfiunibd  45358  hoicvr  46594  0nelsetpreimafv  47429  termchomn0  49524