Theorem neldifsn 4797

Description: The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)

Assertion

Ref	Expression
neldifsn	⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})

Proof of Theorem neldifsn

Step	Hyp	Ref	Expression
1		neirr 2947	. 2 ⊢ ¬ 𝐴 ≠ 𝐴
2		eldifsni 4795	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴 ≠ 𝐴)
3	1, 2	mto 197	1 ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ≠ wne 2938   ∖ cdif 3960  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-dif 3966  df-sn 4632

This theorem is referenced by:  neldifsnd  4798  fofinf1o  9370  dfac9  10175  1div0  11920  xrsupss  13348  hashgt23el  14460  fvsetsid  17202  islbs3  21175  islindf4  21876  ufinffr  23953  i1fd  25730  finsumvtxdg2sstep  29582  matunitlindflem1  37603  poimirlem25  37632  itg2addnclem  37658  itg2addnclem2  37659  prter2  38863  uspgrimprop  47811