Theorem neldifsn 4817

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ≠ wne 2946   ∖ cdif 3973  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-sn 4649

This theorem is referenced by:  neldifsnd  4818  fofinf1o  9400  dfac9  10206  1div0  11949  xrsupss  13371  hashgt23el  14473  fvsetsid  17215  islbs3  21180  islindf4  21881  ufinffr  23958  i1fd  25735  finsumvtxdg2sstep  29585  matunitlindflem1  37576  poimirlem25  37605  itg2addnclem  37631  itg2addnclem2  37632  prter2  38837  uspgrimprop  47757