Theorem neldifsnd 4793

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3948  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627

This theorem is referenced by:  difsnb  4806  fsnunf2  7206  fsumsplit1  15781  rpnnen2lem9  16258  fprodfvdvdsd  16371  ramub1lem1  17064  ramub1lem2  17065  prmdvdsprmo  17080  acsfiindd  18598  gsummgp0  20315  islindf4  21858  gsummatr01lem3  22663  nbgrnself  29376  omsmeas  34325  onint1  36450  bj-fvsnun2  37257  poimirlem30  37657  prtlem80  38862  aks6d1c5lem3  42138  gneispace0nelrn3  44155  supminfxr2  45480  fsumnncl  45587  hoidmv1lelem2  46607  hspmbllem1  46641  hspmbllem2  46642  fsumsplitsndif  47360  isubgr3stgrlem3  47935  mgpsumunsn  48277