Theorem neldifsnd 4749

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-sn 4581

This theorem is referenced by:  difsnb  4762  fsnunf2  7132  fsumsplit1  15668  rpnnen2lem9  16147  fprodfvdvdsd  16261  ramub1lem1  16954  ramub1lem2  16955  prmdvdsprmo  16970  acsfiindd  18476  gsummgp0  20253  islindf4  21793  gsummatr01lem3  22601  nbgrnself  29432  evlextv  33707  esplyindfv  33732  vietalem  33735  omsmeas  34480  onint1  36643  bj-fvsnun2  37457  poimirlem30  37847  prtlem80  39117  aks6d1c5lem3  42387  gneispace0nelrn3  44379  supminfxr2  45709  fsumnncl  45814  hoidmv1lelem2  46832  hspmbllem1  46866  hspmbllem2  46867  fsumsplitsndif  47615  isubgr3stgrlem3  48210  mgpsumunsn  48603