Theorem neldifsnd 4723

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3880  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-sn 4559

This theorem is referenced by:  difsnb  4736  fsnunf2  7040  fsumsplit1  15385  rpnnen2lem9  15859  fprodfvdvdsd  15971  ramub1lem1  16655  ramub1lem2  16656  prmdvdsprmo  16671  acsfiindd  18186  gsummgp0  19762  islindf4  20955  gsummatr01lem3  21714  nbgrnself  27629  omsmeas  32190  onint1  34565  bj-fvsnun2  35354  poimirlem30  35734  prtlem80  36802  gneispace0nelrn3  41641  supminfxr2  42899  fsumnncl  43003  hoidmv1lelem2  44020  hspmbllem1  44054  hspmbllem2  44055  fsumsplitsndif  44713  mgpsumunsn  45585