Theorem neldifsn 4725

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

Syntax hints:  ¬ wn 3   ∈ wcel 2119   ≠ wne 2934   ∖ cdif 3880  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-v 3433  df-dif 3886  df-sn 4556

This theorem is referenced by:  neldifsnd  4726  fofinf1o  9232  dfac9  10050  1div0  11800  xrsupss  13252  hashgt23el  14377  fvsetsid  17129  islbs3  21148  islindf4  21813  ufinffr  23912  i1fd  25666  finsumvtxdg2sstep  29636  matunitlindflem1  37983  poimirlem25  38012  itg2addnclem  38038  itg2addnclem2  38039  prter2  39373