Theorem neldifsn 4760

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

Syntax hints:  ¬ wn 3   ∈ wcel 2143   ≠ wne 2958   ∖ cdif 3902  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-sn 4590

This theorem is referenced by:  neldifsnd  4761  fofinf1o  9285  dfac9  10116  1div0  11868  xrsupss  13330  hashgt23el  14457  fvsetsid  17223  islbs3  21279  islindf4  21988  ufinffr  24086  i1fd  25840  finsumvtxdg2sstep  29899  matunitlindflem1  38287  poimirlem25  38316  itg2addnclem  38342  itg2addnclem2  38343  prter2  39675