Theorem neldifsn 4768

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ≠ wne 2932   ∖ cdif 3923  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-sn 4602

This theorem is referenced by:  neldifsnd  4769  fofinf1o  9344  dfac9  10151  1div0  11896  xrsupss  13325  hashgt23el  14442  fvsetsid  17187  islbs3  21116  islindf4  21798  ufinffr  23867  i1fd  25634  finsumvtxdg2sstep  29529  matunitlindflem1  37640  poimirlem25  37669  itg2addnclem  37695  itg2addnclem2  37696  prter2  38899