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

Theorem neldifsn 3931
Description:  A is not in  ( B  \  { A } ). (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
neldifsn  |-  -.  A  e.  ( B  \  { A } )

Proof of Theorem neldifsn
StepHypRef Expression
1 neirr 2608 . 2  |-  -.  A  =/=  A
2 eldifsni 3930 . 2  |-  ( A  e.  ( B  \  { A } )  ->  A  =/=  A )
31, 2mto 170 1  |-  -.  A  e.  ( B  \  { A } )
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. 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