Theorem n0i 4345

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-dif 3965  df-nul 4339

This theorem is referenced by:  ne0i  4346  n0ii  4348  oprcl  4903  disjss3  5146  elfvdm  6943  mptrcl  7024  isomin  7356  ovrcl  7471  elfvov1  7472  elfvov2  7473  oalimcl  8596  omlimcl  8614  nnaordex2  8675  oaabs2  8685  ecexr  8748  elpmi  8884  elmapex  8886  pmresg  8908  pmsspw  8915  ixpssmap2g  8965  ixpssmapg  8966  resixpfo  8974  php3  9246  php3OLD  9258  cantnfp1lem2  9716  cantnflem1  9726  cnfcom2lem  9738  rankxplim2  9917  rankxplim3  9918  cardlim  10009  alephnbtwn  10108  ttukeylem5  10550  r1wunlim  10774  ssnn0fi  14022  ruclem13  16274  ramtub  17045  elbasfv  17250  elbasov  17251  restsspw  17477  homarcl  18081  grpidval  18686  odlem2  19571  efgrelexlema  19781  subcmn  19869  dvdsrval  20377  elocv  21703  pf1rcl  22368  matrcl  22431  0top  23005  ppttop  23029  pptbas  23030  restrcl  23180  ssrest  23199  iscnp2  23262  lmmo  23403  zfbas  23919  rnelfmlem  23975  isfcls  24032  isnghm  24759  iscau2  25324  itg2cnlem1  25810  itgsubstlem  26103  dchrrcl  27298  clwwlknnn  30061  0ringsubrg  33237  ssdifidllem  33463  ssmxidllem  33480  eulerpartlemgvv  34357  indispconn  35218  cvmtop1  35244  cvmtop2  35245  mrsub0  35500  mrsubf  35501  mrsubccat  35502  mrsubcn  35503  mrsubco  35505  mrsubvrs  35506  msubf  35516  mclsrcl  35545  funpartlem  35923  tailfb  36359  nlpineqsn  37390  atbase  39270  llnbase  39491  lplnbase  39516  lvolbase  39560  osumcllem4N  39941  pexmidlem1N  39952  lhpbase  39980  mapco2g  42701  wepwsolem  43030  onov0suclim  43263  uneqsn  44014  ssfiunibd  45259  hoicvr  46503  0nelsetpreimafv  47314