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

Theorem neldifsn 3931
 Description: is not in . (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
neldifsn

Proof of Theorem neldifsn
StepHypRef Expression
1 neirr 2608 . 2
2 eldifsni 3930 . 2
31, 2mto 170 1
 Colors of variables: wff set class Syntax hints:   wn 3   wcel 1726   wne 2601   cdif 3319  csn 3816 This theorem is referenced by:  neldifsnd  3932  fofinf1o  7390  dfac9  8021  xrsupss  10892  islbs3  16232  ufinffr  17966  i1fd  19576  nbgranself2  21453  itg2addnclem  26270  itg2addnclem2  26271  prter2  26744  uvcff  27231  islindf4  27299 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-sn 3822
 Copyright terms: Public domain W3C validator