Theorem neldifsnd 4759

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 4758	. 2 ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
2	1	a1i 11	1 ⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3899  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-sn 4588

This theorem is used by:  difsnb  4772  fsnunf2  7188  fsumsplit1  15835  rpnnen2lem9  16316  fprodfvdvdsd  16430  ramub1lem1  17124  ramub1lem2  17125  prmdvdsprmo  17140  acsfiindd  18647  gsummgp0  20464  islindf4  22057  gsummatr01lem3  22885  nbgrnself  29827  evlextv  34060  esplyindfv  34094  vietalem  34097  omsmeas  34842  onint1  37076  bj-fvsnun2  38016  poimirlem30  38407  prtlem80  39742  aks6d1c5lem3  43011  gneispace0nelrn3  44990  supminfxr2  46305  fsumnncl  46410  hoidmv1lelem2  47428  hspmbllem1  47462  hspmbllem2  47463  fsumsplitsndif  48277  isubgr3stgrlem3  48892  mgpsumunsn  49299