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

Theorem neldifsn 4792
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 2949 . 2 ¬ 𝐴𝐴
2 eldifsni 4790 . 2 (𝐴 ∈ (𝐵 ∖ {𝐴}) → 𝐴𝐴)
31, 2mto 197 1 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2108  wne 2940  cdif 3948  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627
This theorem is referenced by:  neldifsnd  4793  fofinf1o  9372  dfac9  10177  1div0  11922  xrsupss  13351  hashgt23el  14463  fvsetsid  17205  islbs3  21157  islindf4  21858  ufinffr  23937  i1fd  25716  finsumvtxdg2sstep  29567  matunitlindflem1  37623  poimirlem25  37652  itg2addnclem  37678  itg2addnclem2  37679  prter2  38882  uspgrimprop  47873
  Copyright terms: Public domain W3C validator