Theorem neldifsn 4737

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ≠ wne 2932   ∖ cdif 3886  {csn 4567

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-sn 4568

This theorem is referenced by:  neldifsnd  4738  fofinf1o  9242  dfac9  10059  1div0  11809  xrsupss  13261  hashgt23el  14386  fvsetsid  17138  islbs3  21153  islindf4  21818  ufinffr  23894  i1fd  25648  finsumvtxdg2sstep  29618  matunitlindflem1  37937  poimirlem25  37966  itg2addnclem  37992  itg2addnclem2  37993  prter2  39327