Theorem neldifsnd 4742

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3894  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-sn 4574

This theorem is referenced by:  difsnb  4755  fsnunf2  7120  fsumsplit1  15652  rpnnen2lem9  16131  fprodfvdvdsd  16245  ramub1lem1  16938  ramub1lem2  16939  prmdvdsprmo  16954  acsfiindd  18459  gsummgp0  20236  islindf4  21775  gsummatr01lem3  22572  nbgrnself  29337  omsmeas  34336  onint1  36493  bj-fvsnun2  37300  poimirlem30  37689  prtlem80  38959  aks6d1c5lem3  42229  gneispace0nelrn3  44234  supminfxr2  45566  fsumnncl  45671  hoidmv1lelem2  46689  hspmbllem1  46723  hspmbllem2  46724  fsumsplitsndif  47472  isubgr3stgrlem3  48067  mgpsumunsn  48460