Theorem n0i 3920

Description: If a set 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 3919	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2690	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 317	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 134	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ∈ wcel 1990  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  ne0i  3921  n0ii  3922  oprcl  4427  disjss3  4652  mptrcl  6289  isomin  6587  ovrcl  6686  oalimcl  7640  omlimcl  7658  oaabs2  7725  ecexr  7747  elpmi  7876  elmapex  7878  pmresg  7885  pmsspw  7892  ixpssmap2g  7937  ixpssmapg  7938  resixpfo  7946  php3  8146  cantnfp1lem2  8576  cantnflem1  8586  cnfcom2lem  8598  rankxplim2  8743  rankxplim3  8744  cardlim  8798  alephnbtwn  8894  ttukeylem5  9335  r1wunlim  9559  ssnn0fi  12784  ruclem13  14971  ramtub  15716  elbasfv  15920  elbasov  15921  restsspw  16092  homarcl  16678  grpidval  17260  odlem2  17958  efgrelexlema  18162  subcmn  18242  dvdsrval  18645  pf1rcl  19713  elocv  20012  matrcl  20218  0top  20787  ppttop  20811  pptbas  20812  restrcl  20961  ssrest  20980  iscnp2  21043  lmmo  21184  zfbas  21700  rnelfmlem  21756  isfcls  21813  isnghm  22527  iscau2  23075  itg2cnlem1  23528  itgsubstlem  23811  dchrrcl  24965  eleenn  25776  eulerpartlemgvv  30438  indispconn  31216  cvmtop1  31242  cvmtop2  31243  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  mrsubco  31418  mrsubvrs  31419  msubf  31429  mclsrcl  31458  funpartlem  32049  tailfb  32372  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  osumcllem4N  35245  pexmidlem1N  35256  lhpbase  35284  mapco2g  37277  wepwsolem  37612  uneqsn  38321  ssfiunibd  39523  hoicvr  40762