Theorem neldifsnd 4737

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3887  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  difsnb  4750  fsnunf2  7134  fsumsplit1  15698  rpnnen2lem9  16180  fprodfvdvdsd  16294  ramub1lem1  16988  ramub1lem2  16989  prmdvdsprmo  17004  acsfiindd  18510  gsummgp0  20288  islindf4  21828  gsummatr01lem3  22632  nbgrnself  29442  evlextv  33701  esplyindfv  33735  vietalem  33738  omsmeas  34483  onint1  36647  bj-fvsnun2  37586  poimirlem30  37985  prtlem80  39321  aks6d1c5lem3  42590  gneispace0nelrn3  44587  supminfxr2  45915  fsumnncl  46020  hoidmv1lelem2  47038  hspmbllem1  47072  hspmbllem2  47073  fsumsplitsndif  47841  isubgr3stgrlem3  48456  mgpsumunsn  48849