Theorem neldifsnd 4798

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   ∖ cdif 3960  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-dif 3966  df-sn 4632

This theorem is referenced by:  difsnb  4811  fsnunf2  7206  fsumsplit1  15778  rpnnen2lem9  16255  fprodfvdvdsd  16368  ramub1lem1  17060  ramub1lem2  17061  prmdvdsprmo  17076  acsfiindd  18611  gsummgp0  20332  islindf4  21876  gsummatr01lem3  22679  nbgrnself  29391  omsmeas  34305  onint1  36432  bj-fvsnun2  37239  poimirlem30  37637  prtlem80  38843  aks6d1c5lem3  42119  gneispace0nelrn3  44132  supminfxr2  45419  fsumnncl  45528  hoidmv1lelem2  46548  hspmbllem1  46582  hspmbllem2  46583  fsumsplitsndif  47298  isubgr3stgrlem3  47871  mgpsumunsn  48206