Theorem neldifsn 4750

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

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

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 3444  df-dif 3906  df-sn 4583

This theorem is referenced by:  neldifsnd  4751  fofinf1o  9244  dfac9  10059  1div0  11808  xrsupss  13236  hashgt23el  14359  fvsetsid  17107  islbs3  21122  islindf4  21805  ufinffr  23885  i1fd  25650  finsumvtxdg2sstep  29635  matunitlindflem1  37867  poimirlem25  37896  itg2addnclem  37922  itg2addnclem2  37923  prter2  39257