Theorem neldifsnd 4757

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3911  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-sn 4590

This theorem is referenced by:  difsnb  4770  fsnunf2  7160  fsumsplit1  15711  rpnnen2lem9  16190  fprodfvdvdsd  16304  ramub1lem1  16997  ramub1lem2  16998  prmdvdsprmo  17013  acsfiindd  18512  gsummgp0  20227  islindf4  21747  gsummatr01lem3  22544  nbgrnself  29286  omsmeas  34314  onint1  36437  bj-fvsnun2  37244  poimirlem30  37644  prtlem80  38854  aks6d1c5lem3  42125  gneispace0nelrn3  44131  supminfxr2  45465  fsumnncl  45570  hoidmv1lelem2  46590  hspmbllem1  46624  hspmbllem2  46625  fsumsplitsndif  47374  isubgr3stgrlem3  47967  mgpsumunsn  48349