Theorem neldifsn 4741

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111   ≠ wne 2928   ∖ cdif 3894  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-sn 4574

This theorem is referenced by:  neldifsnd  4742  fofinf1o  9216  dfac9  10028  1div0  11776  xrsupss  13208  hashgt23el  14331  fvsetsid  17079  islbs3  21092  islindf4  21775  ufinffr  23844  i1fd  25609  finsumvtxdg2sstep  29528  matunitlindflem1  37666  poimirlem25  37695  itg2addnclem  37721  itg2addnclem2  37722  prter2  38990