Theorem n0i 4299

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 4296	. . 3 ⊢ ¬ 𝐵 ∈ ∅
2		eleq2 2901	. . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅))
3	1, 2	mtbiri 329	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
4	3	con2i 141	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

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

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3939  df-nul 4292

This theorem is referenced by:  ne0i  4300  n0ii  4302  oprcl  4829  disjss3  5065  elfvdm  6702  mptrcl  6777  isomin  7090  ovrcl  7197  oalimcl  8186  omlimcl  8204  oaabs2  8272  ecexr  8294  elpmi  8425  elmapex  8427  pmresg  8434  pmsspw  8441  ixpssmap2g  8491  ixpssmapg  8492  resixpfo  8500  php3  8703  cantnfp1lem2  9142  cantnflem1  9152  cnfcom2lem  9164  rankxplim2  9309  rankxplim3  9310  cardlim  9401  alephnbtwn  9497  ttukeylem5  9935  r1wunlim  10159  ssnn0fi  13354  ruclem13  15595  ramtub  16348  elbasfv  16544  elbasov  16545  restsspw  16705  homarcl  17288  grpidval  17871  odlem2  18667  efgrelexlema  18875  subcmn  18957  dvdsrval  19395  pf1rcl  20512  elocv  20812  matrcl  21021  0top  21591  ppttop  21615  pptbas  21616  restrcl  21765  ssrest  21784  iscnp2  21847  lmmo  21988  zfbas  22504  rnelfmlem  22560  isfcls  22617  isnghm  23332  iscau2  23880  itg2cnlem1  24362  itgsubstlem  24645  dchrrcl  25816  clwwlknnn  27811  ssmxidllem  30978  eulerpartlemgvv  31634  indispconn  32481  cvmtop1  32507  cvmtop2  32508  mrsub0  32763  mrsubf  32764  mrsubccat  32765  mrsubcn  32766  mrsubco  32768  mrsubvrs  32769  msubf  32779  mclsrcl  32808  funpartlem  33403  tailfb  33725  nlpineqsn  34692  atbase  36440  llnbase  36660  lplnbase  36685  lvolbase  36729  osumcllem4N  37110  pexmidlem1N  37121  lhpbase  37149  mapco2g  39360  wepwsolem  39691  uneqsn  40422  ssfiunibd  41625  hoicvr  42879  0nelsetpreimafv  43599