Theorem neldifsn 4752

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3908  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-sn 4586

This theorem is referenced by:  neldifsnd  4753  fofinf1o  9259  dfac9  10066  1div0  11813  xrsupss  13245  hashgt23el  14365  fvsetsid  17114  islbs3  21041  islindf4  21723  ufinffr  23792  i1fd  25558  finsumvtxdg2sstep  29453  matunitlindflem1  37583  poimirlem25  37612  itg2addnclem  37638  itg2addnclem2  37639  prter2  38847