Theorem neldifsnd 4756

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3896  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-sn 4585

This theorem is used by:  difsnb  4769  fsnunf2  7185  fsumsplit1  15832  rpnnen2lem9  16311  fprodfvdvdsd  16425  ramub1lem1  17119  ramub1lem2  17120  prmdvdsprmo  17135  acsfiindd  18642  gsummgp0  20459  islindf4  22052  gsummatr01lem3  22880  nbgrnself  29820  evlextv  34053  esplyindfv  34087  vietalem  34090  omsmeas  34835  onint1  37069  bj-fvsnun2  38009  poimirlem30  38400  prtlem80  39735  aks6d1c5lem3  43004  gneispace0nelrn3  44983  supminfxr2  46298  fsumnncl  46403  hoidmv1lelem2  47421  hspmbllem1  47455  hspmbllem2  47456  fsumsplitsndif  48270  isubgr3stgrlem3  48885  mgpsumunsn  49292