Theorem neldifsnd 4796

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

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

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3951  df-sn 4629

This theorem is referenced by:  difsnb  4809  fsnunf2  7186  fsumsplit1  15693  rpnnen2lem9  16167  fprodfvdvdsd  16279  ramub1lem1  16961  ramub1lem2  16962  prmdvdsprmo  16977  acsfiindd  18508  gsummgp0  20134  islindf4  21399  gsummatr01lem3  22166  nbgrnself  28654  omsmeas  33391  onint1  35420  bj-fvsnun2  36223  poimirlem30  36604  prtlem80  37817  gneispace0nelrn3  42975  supminfxr2  44258  fsumnncl  44367  hoidmv1lelem2  45387  hspmbllem1  45421  hspmbllem2  45422  fsumsplitsndif  46120  mgpsumunsn  47116