Theorem neldifsnd 4726

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-v 3434  df-dif 3890  df-sn 4562

This theorem is referenced by:  difsnb  4739  fsnunf2  7058  fsumsplit1  15457  rpnnen2lem9  15931  fprodfvdvdsd  16043  ramub1lem1  16727  ramub1lem2  16728  prmdvdsprmo  16743  acsfiindd  18271  gsummgp0  19847  islindf4  21045  gsummatr01lem3  21806  nbgrnself  27726  omsmeas  32290  onint1  34638  bj-fvsnun2  35427  poimirlem30  35807  prtlem80  36875  gneispace0nelrn3  41752  supminfxr2  43009  fsumnncl  43113  hoidmv1lelem2  44130  hspmbllem1  44164  hspmbllem2  44165  fsumsplitsndif  44825  mgpsumunsn  45697