Theorem neldifsn 4764

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

Syntax hints:  ¬ wn 3   ∈ wcel 2149   ≠ wne 2964   ∖ cdif 3910  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-sn 4595

This theorem is referenced by:  neldifsnd  4765  fofinf1o  9289  dfac9  10120  1div0  11873  xrsupss  13335  hashgt23el  14461  fvsetsid  17228  islbs3  21257  islindf4  21957  ufinffr  24055  i1fd  25809  finsumvtxdg2sstep  29840  matunitlindflem1  38155  poimirlem25  38184  itg2addnclem  38210  itg2addnclem2  38211  prter2  39545