Theorem n0i 4294

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4287

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-nul 4288

This theorem is referenced by:  ne0i  4295  n0ii  4297  oprcl  4857  disjss3  5099  elfvdm  6876  mptrcl  6959  isomin  7293  ovrcl  7409  elfvov1  7410  elfvov2  7411  oalimcl  8497  omlimcl  8515  nnaordex2  8577  oaabs2  8587  ecexr  8650  elpmi  8795  elmapex  8797  pmresg  8820  pmsspw  8827  ixpssmap2g  8877  ixpssmapg  8878  resixpfo  8886  php3  9145  cantnfp1lem2  9600  cantnflem1  9610  cnfcom2lem  9622  rankxplim2  9804  rankxplim3  9805  cardlim  9896  alephnbtwn  9993  ttukeylem5  10435  r1wunlim  10660  ssnn0fi  13920  ruclem13  16179  ramtub  16952  elbasfv  17154  elbasov  17155  restsspw  17363  homarcl  17964  grpidval  18598  odlem2  19480  efgrelexlema  19690  subcmn  19778  dvdsrval  20309  elocv  21635  pf1rcl  22305  matrcl  22368  0top  22939  ppttop  22963  pptbas  22964  restrcl  23113  ssrest  23132  iscnp2  23195  lmmo  23336  zfbas  23852  rnelfmlem  23908  isfcls  23965  isnghm  24679  iscau2  25245  itg2cnlem1  25730  itgsubstlem  26023  dchrrcl  27219  clwwlknnn  30120  0ringsubrg  33345  ssdifidllem  33549  ssmxidllem  33566  eulerpartlemgvv  34554  indispconn  35450  cvmtop1  35476  cvmtop2  35477  mrsub0  35732  mrsubf  35733  mrsubccat  35734  mrsubcn  35735  mrsubco  35737  mrsubvrs  35738  msubf  35748  mclsrcl  35777  funpartlem  36158  tailfb  36593  nlpineqsn  37663  atbase  39665  llnbase  39885  lplnbase  39910  lvolbase  39954  osumcllem4N  40335  pexmidlem1N  40346  lhpbase  40374  mapco2g  43071  wepwsolem  43399  onov0suclim  43631  uneqsn  44381  relpmin  45308  ssfiunibd  45671  hoicvr  46906  0nelsetpreimafv  47750  termchomn0  49843