Theorem neldifsnd 4774

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-v 3466  df-dif 3934  df-sn 4607

This theorem is referenced by:  difsnb  4787  fsnunf2  7183  fsumsplit1  15766  rpnnen2lem9  16245  fprodfvdvdsd  16358  ramub1lem1  17051  ramub1lem2  17052  prmdvdsprmo  17067  acsfiindd  18568  gsummgp0  20283  islindf4  21803  gsummatr01lem3  22600  nbgrnself  29343  omsmeas  34360  onint1  36472  bj-fvsnun2  37279  poimirlem30  37679  prtlem80  38884  aks6d1c5lem3  42155  gneispace0nelrn3  44133  supminfxr2  45463  fsumnncl  45568  hoidmv1lelem2  46588  hspmbllem1  46622  hspmbllem2  46623  fsumsplitsndif  47354  isubgr3stgrlem3  47947  mgpsumunsn  48303