Theorem neldifsn 4736

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3887  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  neldifsnd  4737  fofinf1o  9236  dfac9  10053  1div0  11803  xrsupss  13255  hashgt23el  14380  fvsetsid  17132  islbs3  21148  islindf4  21831  ufinffr  23907  i1fd  25661  finsumvtxdg2sstep  29636  matunitlindflem1  37954  poimirlem25  37983  itg2addnclem  38009  itg2addnclem2  38010  prter2  39344