Theorem neldifsnd 4762

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   ∖ cdif 3903  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3909  df-sn 4591

This theorem is referenced by:  difsnb  4775  fsnunf2  7186  fsumsplit1  15798  rpnnen2lem9  16279  fprodfvdvdsd  16393  ramub1lem1  17087  ramub1lem2  17088  prmdvdsprmo  17103  acsfiindd  18610  gsummgp0  20400  islindf4  21969  gsummatr01lem3  22795  nbgrnself  29687  evlextv  33910  esplyindfv  33944  vietalem  33947  omsmeas  34691  onint1  36938  bj-fvsnun2  37878  poimirlem30  38279  prtlem80  39613  aks6d1c5lem3  42882  gneispace0nelrn3  44848  supminfxr2  46163  fsumnncl  46268  hoidmv1lelem2  47286  hspmbllem1  47320  hspmbllem2  47321  fsumsplitsndif  48095  isubgr3stgrlem3  48710  mgpsumunsn  49118