Theorem neldifsnd 4322

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1990   ∖ cdif 3571  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-sn 4178

This theorem is referenced by:  difsnb  4337  fsnunf2  6452  rpnnen2lem9  14951  fprodfvdvdsd  15058  ramub1lem1  15730  ramub1lem2  15731  prmdvdsprmo  15746  acsfiindd  17177  gsummgp0  18608  islindf4  20177  gsummatr01lem3  20463  nbgrnself  26257  omsmeas  30385  onint1  32448  poimirlem30  33439  prtlem80  34146  gneispace0nelrn3  38440  supminfxr2  39699  fsumnncl  39803  fsumsplit1  39804  hoidmv1lelem2  40806  hspmbllem1  40840  hspmbllem2  40841  fsumsplitsndif  41343  mgpsumunsn  42140