Theorem neldifsnd 4745

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3899  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3905  df-sn 4577

This theorem is referenced by:  difsnb  4758  fsnunf2  7120  fsumsplit1  15649  rpnnen2lem9  16128  fprodfvdvdsd  16242  ramub1lem1  16935  ramub1lem2  16936  prmdvdsprmo  16951  acsfiindd  18456  gsummgp0  20234  islindf4  21773  gsummatr01lem3  22570  nbgrnself  29335  omsmeas  34331  onint1  36482  bj-fvsnun2  37289  poimirlem30  37689  prtlem80  38899  aks6d1c5lem3  42169  gneispace0nelrn3  44174  supminfxr2  45506  fsumnncl  45611  hoidmv1lelem2  46629  hspmbllem1  46663  hspmbllem2  46664  fsumsplitsndif  47403  isubgr3stgrlem3  47998  mgpsumunsn  48391