Theorem neldifsn 4746

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ≠ wne 2930   ∖ cdif 3896  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-sn 4579

This theorem is referenced by:  neldifsnd  4747  fofinf1o  9230  dfac9  10045  1div0  11794  xrsupss  13222  hashgt23el  14345  fvsetsid  17093  islbs3  21108  islindf4  21791  ufinffr  23871  i1fd  25636  finsumvtxdg2sstep  29572  matunitlindflem1  37756  poimirlem25  37785  itg2addnclem  37811  itg2addnclem2  37812  prter2  39080