Theorem neldifsn 4754

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2144   ≠ wne 2955   ∖ cdif 4045  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-sn 4584

This theorem is used by:  neldifsnd  4755  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  38564  itg2addnclem  38590  itg2addnclem2  38591  prter2  39939