Theorem neldifsnd 4766

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   ∖ cdif 3905  {csn 4594

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-v 3460  df-dif 3911  df-sn 4595

This theorem is used by:  difsnb  4779  fsnunf2  7191  fsumsplit1  15822  rpnnen2lem9  16303  fprodfvdvdsd  16417  ramub1lem1  17111  ramub1lem2  17112  prmdvdsprmo  17127  acsfiindd  18634  gsummgp0  20432  islindf4  22025  gsummatr01lem3  22851  nbgrnself  29746  evlextv  33963  esplyindfv  33997  vietalem  34000  omsmeas  34745  onint1  37001  bj-fvsnun2  37941  poimirlem30  38342  prtlem80  39676  aks6d1c5lem3  42945  gneispace0nelrn3  44909  supminfxr2  46224  fsumnncl  46329  hoidmv1lelem2  47347  hspmbllem1  47381  hspmbllem2  47382  fsumsplitsndif  48159  isubgr3stgrlem3  48774  mgpsumunsn  49182