Theorem neldifsnd 4818

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3973  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-sn 4649

This theorem is referenced by:  difsnb  4831  fsnunf2  7220  fsumsplit1  15793  rpnnen2lem9  16270  fprodfvdvdsd  16382  ramub1lem1  17073  ramub1lem2  17074  prmdvdsprmo  17089  acsfiindd  18623  gsummgp0  20341  islindf4  21881  gsummatr01lem3  22684  nbgrnself  29394  omsmeas  34288  onint1  36415  bj-fvsnun2  37222  poimirlem30  37610  prtlem80  38817  aks6d1c5lem3  42094  gneispace0nelrn3  44104  supminfxr2  45384  fsumnncl  45493  hoidmv1lelem2  46513  hspmbllem1  46547  hspmbllem2  46548  fsumsplitsndif  47247  mgpsumunsn  48086