Theorem neldifsnd 4797

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3946  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-sn 4630

This theorem is referenced by:  difsnb  4810  fsnunf2  7184  fsumsplit1  15691  rpnnen2lem9  16165  fprodfvdvdsd  16277  ramub1lem1  16959  ramub1lem2  16960  prmdvdsprmo  16975  acsfiindd  18506  gsummgp0  20130  islindf4  21393  gsummatr01lem3  22159  nbgrnself  28616  omsmeas  33322  onint1  35334  bj-fvsnun2  36137  poimirlem30  36518  prtlem80  37731  gneispace0nelrn3  42893  supminfxr2  44179  fsumnncl  44288  hoidmv1lelem2  45308  hspmbllem1  45342  hspmbllem2  45343  fsumsplitsndif  46041  mgpsumunsn  47037