Theorem neldifsn 4759

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ≠ wne 2926   ∖ cdif 3914  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-sn 4593

This theorem is referenced by:  neldifsnd  4760  fofinf1o  9290  dfac9  10097  1div0  11844  xrsupss  13276  hashgt23el  14396  fvsetsid  17145  islbs3  21072  islindf4  21754  ufinffr  23823  i1fd  25589  finsumvtxdg2sstep  29484  matunitlindflem1  37617  poimirlem25  37646  itg2addnclem  37672  itg2addnclem2  37673  prter2  38881