Theorem neldifsn 4792

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ≠ wne 2940   ∖ cdif 3948  {csn 4626

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627

This theorem is referenced by:  neldifsnd  4793  fofinf1o  9372  dfac9  10177  1div0  11922  xrsupss  13351  hashgt23el  14463  fvsetsid  17205  islbs3  21157  islindf4  21858  ufinffr  23937  i1fd  25716  finsumvtxdg2sstep  29567  matunitlindflem1  37623  poimirlem25  37652  itg2addnclem  37678  itg2addnclem2  37679  prter2  38882  uspgrimprop  47873