Theorem neldifsn 4719

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

Syntax hints:  ¬ wn 3   ∈ wcel 2110   ≠ wne 3016   ∖ cdif 3933  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3497  df-dif 3939  df-sn 4562

This theorem is referenced by:  neldifsnd  4720  fofinf1o  8793  dfac9  9556  xrsupss  12696  hashgt23el  13779  fvsetsid  16509  islbs3  19921  islindf4  20976  ufinffr  22531  i1fd  24276  finsumvtxdg2sstep  27325  matunitlindflem1  34882  poimirlem25  34911  itg2addnclem  34937  itg2addnclem2  34938  prter2  36011