Theorem neldifsnd 4752

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141   ∖ cdif 3901  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3907  df-sn 4582

This theorem is referenced by:  difsnb  4765  fsnunf2  7166  fsumsplit1  15755  rpnnen2lem9  16237  fprodfvdvdsd  16351  ramub1lem1  17045  ramub1lem2  17046  prmdvdsprmo  17061  acsfiindd  18568  gsummgp0  20345  islindf4  21870  gsummatr01lem3  22697  nbgrnself  29506  evlextv  33800  esplyindfv  33834  vietalem  33837  omsmeas  34581  onint1  36773  bj-fvsnun2  37712  poimirlem30  38113  prtlem80  39449  aks6d1c5lem3  42718  gneispace0nelrn3  44682  supminfxr2  46007  fsumnncl  46112  hoidmv1lelem2  47130  hspmbllem1  47164  hspmbllem2  47165  fsumsplitsndif  47939  isubgr3stgrlem3  48554  mgpsumunsn  48947