Theorem neldifsn 4743

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3900  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-sn 4578

This theorem is referenced by:  neldifsnd  4744  fofinf1o  9222  dfac9  10031  1div0  11779  xrsupss  13211  hashgt23el  14331  fvsetsid  17079  islbs3  21062  islindf4  21745  ufinffr  23814  i1fd  25580  finsumvtxdg2sstep  29495  matunitlindflem1  37600  poimirlem25  37629  itg2addnclem  37655  itg2addnclem2  37656  prter2  38864