Theorem neldifsn 4725

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ≠ wne 2943   ∖ cdif 3884  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-v 3434  df-dif 3890  df-sn 4562

This theorem is referenced by:  neldifsnd  4726  fofinf1o  9094  dfac9  9892  xrsupss  13043  hashgt23el  14139  fvsetsid  16869  islbs3  20417  islindf4  21045  ufinffr  23080  i1fd  24845  finsumvtxdg2sstep  27916  matunitlindflem1  35773  poimirlem25  35802  itg2addnclem  35828  itg2addnclem2  35829  prter2  36895