Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neldifsn Structured version   Visualization version   GIF version

Theorem neldifsn 4685
 Description: The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
neldifsn ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})

Proof of Theorem neldifsn
StepHypRef Expression
1 neirr 2996 . 2 ¬ 𝐴𝐴
2 eldifsni 4683 . 2 (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴𝐴)
31, 2mto 200 1 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∈ wcel 2111   ≠ wne 2987   ∖ cdif 3878  {csn 4525 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-dif 3884  df-sn 4526 This theorem is referenced by:  neldifsnd  4686  fofinf1o  8786  dfac9  9550  xrsupss  12693  hashgt23el  13784  fvsetsid  16510  islbs3  19924  islindf4  20532  ufinffr  22544  i1fd  24295  finsumvtxdg2sstep  27349  matunitlindflem1  35072  poimirlem25  35101  itg2addnclem  35127  itg2addnclem2  35128  prter2  36196
 Copyright terms: Public domain W3C validator