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

Theorem neldifsn 4465
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 2939 . 2 ¬ 𝐴𝐴
2 eldifsni 4464 . 2 (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴𝐴)
31, 2mto 188 1 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2137  wne 2930  cdif 3710  {csn 4319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-v 3340  df-dif 3716  df-sn 4320
This theorem is referenced by:  neldifsnd  4466  fofinf1o  8404  dfac9  9148  xrsupss  12330  fvsetsid  16090  islbs3  19355  islindf4  20377  ufinffr  21932  i1fd  23645  finsumvtxdg2sstep  26653  matunitlindflem1  33716  poimirlem25  33745  itg2addnclem  33772  itg2addnclem2  33773  prter2  34668
  Copyright terms: Public domain W3C validator