Theorem neldifsn 4705

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

Syntax hints:  ¬ wn 3   ∈ wcel 2110   ≠ wne 2940   ∖ cdif 3863  {csn 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3410  df-dif 3869  df-sn 4542

This theorem is referenced by:  neldifsnd  4706  fofinf1o  8951  dfac9  9750  xrsupss  12899  hashgt23el  13991  fvsetsid  16721  islbs3  20192  islindf4  20800  ufinffr  22826  i1fd  24578  finsumvtxdg2sstep  27637  matunitlindflem1  35510  poimirlem25  35539  itg2addnclem  35565  itg2addnclem2  35566  prter2  36632