Theorem neldifsnd 4751

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

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

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 3444  df-dif 3906  df-sn 4583

This theorem is referenced by:  difsnb  4764  fsnunf2  7142  fsumsplit1  15680  rpnnen2lem9  16159  fprodfvdvdsd  16273  ramub1lem1  16966  ramub1lem2  16967  prmdvdsprmo  16982  acsfiindd  18488  gsummgp0  20265  islindf4  21805  gsummatr01lem3  22613  nbgrnself  29444  evlextv  33718  esplyindfv  33752  vietalem  33755  omsmeas  34500  onint1  36662  bj-fvsnun2  37505  poimirlem30  37895  prtlem80  39231  aks6d1c5lem3  42501  gneispace0nelrn3  44492  supminfxr2  45821  fsumnncl  45926  hoidmv1lelem2  46944  hspmbllem1  46978  hspmbllem2  46979  fsumsplitsndif  47727  isubgr3stgrlem3  48322  mgpsumunsn  48715