Theorem neldifsn 4754

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146   ≠ wne 2958   ∖ cdif 4047  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3455  df-dif 4049  df-sn 4588

This theorem is used by:  neldifsnd  4755  fofinf1o  9332  dfac9  10225  1div0  11985  xrsupss  13449  hashgt23el  14579  fvsetsid  17358  islbs3  21445  islindf4  22156  matunitlindflem1  23006  ufinffr  24260  i1fd  26014  finsumvtxdg2sstep  30142  poimirlem25  38703  itg2addnclem  38729  itg2addnclem2  38730  prter2  40078