Theorem neldifsnd 4744

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ∖ cdif 3895  {csn 4575

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-v 3439  df-dif 3901  df-sn 4576

This theorem is referenced by:  difsnb  4757  fsnunf2  7126  fsumsplit1  15654  rpnnen2lem9  16133  fprodfvdvdsd  16247  ramub1lem1  16940  ramub1lem2  16941  prmdvdsprmo  16956  acsfiindd  18461  gsummgp0  20238  islindf4  21777  gsummatr01lem3  22573  nbgrnself  29339  omsmeas  34357  onint1  36514  bj-fvsnun2  37321  poimirlem30  37710  prtlem80  38980  aks6d1c5lem3  42250  gneispace0nelrn3  44259  supminfxr2  45591  fsumnncl  45696  hoidmv1lelem2  46714  hspmbllem1  46748  hspmbllem2  46749  fsumsplitsndif  47497  isubgr3stgrlem3  48092  mgpsumunsn  48485