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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-sn 4585

This theorem is used by:  difsnb  4769  fsnunf2  7183  fsumsplit1  15891  rpnnen2lem9  16370  fprodfvdvdsd  16484  ramub1lem1  17184  ramub1lem2  17185  prmdvdsprmo  17200  acsfiindd  18707  gsummgp0  20527  islindf4  22124  gsummatr01lem3  22952  nbgrnself  29922  evlextv  34156  esplyindfv  34190  vietalem  34193  omsmeas  34938  onint1  37207  bj-fvsnun2  38145  poimirlem30  38536  prtlem80  39886  aks6d1c5lem3  43155  gneispace0nelrn3  45101  supminfxr2  46423  fsumnncl  46528  hoidmv1lelem2  47546  hspmbllem1  47580  hspmbllem2  47581  fsumsplitsndif  48395  isubgr3stgrlem3  49010  mgpsumunsn  49417