Theorem neldifsn 4757

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2147   ≠ wne 2959   ∖ cdif 4048  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-sn 4589

This theorem is used by:  neldifsnd  4758  fofinf1o  9359  dfac9  10254  1div0  12015  xrsupss  13479  hashgt23el  14610  fvsetsid  17390  islbs3  21484  islindf4  22199  matunitlindflem1  23049  ufinffr  24303  i1fd  26057  finsumvtxdg2sstep  30187  poimirlem25  38831  itg2addnclem  38857  itg2addnclem2  38858  prter2  40204