Theorem neldifsnd 4733

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-sn 4563

This theorem is referenced by:  difsnb  4746  fsnunf2  7137  fsumsplit1  15705  rpnnen2lem9  16187  fprodfvdvdsd  16301  ramub1lem1  16995  ramub1lem2  16996  prmdvdsprmo  17011  acsfiindd  18517  gsummgp0  20295  islindf4  21820  gsummatr01lem3  22647  nbgrnself  29453  evlextv  33733  esplyindfv  33767  vietalem  33770  omsmeas  34514  onint1  36684  bj-fvsnun2  37623  poimirlem30  38024  prtlem80  39360  aks6d1c5lem3  42629  gneispace0nelrn3  44593  supminfxr2  45919  fsumnncl  46024  hoidmv1lelem2  47042  hspmbllem1  47076  hspmbllem2  47077  fsumsplitsndif  47851  isubgr3stgrlem3  48466  mgpsumunsn  48859