Theorem neldifsnd 4758

Description: The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)

Assertion

Ref	Expression
neldifsnd	⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))

Proof of Theorem neldifsnd

Step	Hyp	Ref	Expression
1		neldifsn 4757	. 2 ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
2	1	a1i 11	1 ⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   ∖ cdif 3910  {csn 4591

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3448  df-dif 3916  df-sn 4592

This theorem is referenced by:  difsnb  4771  fsnunf2  7137  fsumsplit1  15641  rpnnen2lem9  16115  fprodfvdvdsd  16227  ramub1lem1  16909  ramub1lem2  16910  prmdvdsprmo  16925  acsfiindd  18456  gsummgp0  20046  islindf4  21281  gsummatr01lem3  22043  nbgrnself  28370  omsmeas  33012  onint1  34997  bj-fvsnun2  35800  poimirlem30  36181  prtlem80  37396  gneispace0nelrn3  42536  supminfxr2  43824  fsumnncl  43933  hoidmv1lelem2  44953  hspmbllem1  44987  hspmbllem2  44988  fsumsplitsndif  45685  mgpsumunsn  46557