Theorem neldifsnd 4756

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147   ∖ cdif 4048  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-sn 4589

This theorem is used by:  difsnb  4769  fsnunf2  7217  fsumsplit1  15943  rpnnen2lem9  16422  fprodfvdvdsd  16536  ramub1lem1  17236  ramub1lem2  17237  prmdvdsprmo  17252  acsfiindd  18759  gsummgp0  20580  islindf4  22177  gsummatr01lem3  23005  nbgrnself  29973  evlextv  34257  esplyindfv  34291  vietalem  34294  omsmeas  35038  onint1  37428  bj-fvsnun2  38382  poimirlem30  38773  prtlem80  40121  aks6d1c5lem3  43390  gneispace0nelrn3  45345  supminfxr2  46694  fsumnncl  46799  hoidmv1lelem2  47817  hspmbllem1  47851  hspmbllem2  47852  fsumsplitsndif  48666  isubgr3stgrlem3  49281  mgpsumunsn  49688