Theorem neldifsn 4796

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

Syntax hints:  ¬ wn 3   ∈ wcel 2107   ≠ wne 2941   ∖ cdif 3946  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-sn 4630

This theorem is referenced by:  neldifsnd  4797  fofinf1o  9327  dfac9  10131  xrsupss  13288  hashgt23el  14384  fvsetsid  17101  islbs3  20768  islindf4  21393  ufinffr  23433  i1fd  25198  finsumvtxdg2sstep  28806  matunitlindflem1  36484  poimirlem25  36513  itg2addnclem  36539  itg2addnclem2  36540  prter2  37751