Theorem neldifsn 4757

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

Syntax hints:  ¬ wn 3   ∈ wcel 2106   ≠ wne 2939   ∖ cdif 3910  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3448  df-dif 3916  df-sn 4592

This theorem is referenced by:  neldifsnd  4758  fofinf1o  9278  dfac9  10081  xrsupss  13238  hashgt23el  14334  fvsetsid  17051  islbs3  20675  islindf4  21281  ufinffr  23317  i1fd  25082  finsumvtxdg2sstep  28560  matunitlindflem1  36147  poimirlem25  36176  itg2addnclem  36202  itg2addnclem2  36203  prter2  37416