Theorem neldifsnd 4738

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-sn 4568

This theorem is referenced by:  difsnb  4751  fsnunf2  7141  fsumsplit1  15707  rpnnen2lem9  16189  fprodfvdvdsd  16303  ramub1lem1  16997  ramub1lem2  16998  prmdvdsprmo  17013  acsfiindd  18519  gsummgp0  20297  islindf4  21818  gsummatr01lem3  22622  nbgrnself  29428  evlextv  33686  esplyindfv  33720  vietalem  33723  omsmeas  34467  onint1  36631  bj-fvsnun2  37570  poimirlem30  37971  prtlem80  39307  aks6d1c5lem3  42576  gneispace0nelrn3  44569  supminfxr2  45897  fsumnncl  46002  hoidmv1lelem2  47020  hspmbllem1  47054  hspmbllem2  47055  fsumsplitsndif  47829  isubgr3stgrlem3  48444  mgpsumunsn  48837