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

Syntax hints:  ¬ wn 3   ∈ wcel 2142   ≠ wne 2957   ∖ cdif 3901  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-sn 4583

This theorem is referenced by:  neldifsnd  4753  fofinf1o  9275  dfac9  10093  1div0  11846  xrsupss  13312  hashgt23el  14437  fvsetsid  17204  islbs3  21225  islindf4  21890  ufinffr  23989  i1fd  25743  finsumvtxdg2sstep  29750  matunitlindflem1  38115  poimirlem25  38144  itg2addnclem  38170  itg2addnclem2  38171  prter2  39505