Theorem neldifsn 4755

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145   ≠ wne 2956   ∖ cdif 3896  {csn 4584

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-sn 4585

This theorem is used by:  neldifsnd  4756  fofinf1o  9321  dfac9  10215  1div0  11975  xrsupss  13439  hashgt23el  14569  fvsetsid  17346  islbs3  21433  islindf4  22144  matunitlindflem1  22994  ufinffr  24248  i1fd  26002  finsumvtxdg2sstep  30130  poimirlem25  38563  itg2addnclem  38589  itg2addnclem2  38590  prter2  39938