Theorem neldifsnd 4752

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 4045  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-sn 4585

This theorem is used by:  difsnb  4765  fsnunf2  7191  fsumsplit1  15916  rpnnen2lem9  16395  fprodfvdvdsd  16509  ramub1lem1  17209  ramub1lem2  17210  prmdvdsprmo  17225  acsfiindd  18732  gsummgp0  20552  islindf4  22149  gsummatr01lem3  22977  nbgrnself  29945  evlextv  34220  esplyindfv  34254  vietalem  34257  omsmeas  35001  onint1  37329  bj-fvsnun2  38270  poimirlem30  38661  prtlem80  40011  aks6d1c5lem3  43280  gneispace0nelrn3  45235  supminfxr2  46572  fsumnncl  46677  hoidmv1lelem2  47695  hspmbllem1  47729  hspmbllem2  47730  fsumsplitsndif  48544  isubgr3stgrlem3  49159  mgpsumunsn  49566