Theorem neldifsn 4730

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 2948	. 2 ⊢ ¬ 𝐴 ≠ 𝐴
2		eldifsni 4728	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴 ≠ 𝐴)
3	1, 2	mto 196	1 ⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})

Syntax hints:  ¬ wn 3   ∈ wcel 2103   ≠ wne 2939   ∖ cdif 3888  {csn 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1541  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2940  df-v 3438  df-dif 3894  df-sn 4565

This theorem is referenced by:  neldifsnd  4731  fofinf1o  9152  dfac9  9952  xrsupss  13103  hashgt23el  14198  fvsetsid  16928  islbs3  20480  islindf4  21108  ufinffr  23143  i1fd  24908  finsumvtxdg2sstep  28014  matunitlindflem1  35831  poimirlem25  35860  itg2addnclem  35886  itg2addnclem2  35887  prter2  37105