Theorem neldifsn 4762

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146   ≠ wne 2960   ∖ cdif 3903  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-sn 4592

This theorem is used by:  neldifsnd  4763  fofinf1o  9296  dfac9  10136  1div0  11890  xrsupss  13353  hashgt23el  14481  fvsetsid  17252  islbs3  21331  islindf4  22040  ufinffr  24139  i1fd  25893  finsumvtxdg2sstep  29959  matunitlindflem1  38326  poimirlem25  38355  itg2addnclem  38381  itg2addnclem2  38382  prter2  39715