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

Theorem dif1o 6515
Description: Two ways to say that  A is a nonzero number of the set  B. (Contributed by Mario Carneiro, 21-May-2015.)
Assertion
Ref Expression
dif1o  |-  ( A  e.  ( B  \  1o )  <->  ( A  e.  B  /\  A  =/=  (/) ) )

Proof of Theorem dif1o
StepHypRef Expression
1 df1o2 6507 . . . 4  |-  1o  =  { (/) }
21difeq2i 3304 . . 3  |-  ( B 
\  1o )  =  ( B  \  { (/)
} )
32eleq2i 2360 . 2  |-  ( A  e.  ( B  \  1o )  <->  A  e.  ( B  \  { (/) } ) )
4 eldifsn 3762 . 2  |-  ( A  e.  ( B  \  { (/) } )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
53, 4bitri 240 1  |-  ( A  e.  ( B  \  1o )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1696    =/= wne 2459    \ cdif 3162   (/)c0 3468   {csn 3653   1oc1o 6488
This theorem is referenced by:  ondif1  6516  brwitnlem  6522  oelim2  6609  oeeulem  6615  oeeui  6616  omabs  6661  cantnfle  7388  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnfp1  7399  oemapvali  7402  cantnflem1a  7403  cantnflem1c  7405  cantnflem1  7407  cantnflem3  7409  cantnflem4  7410  cantnf  7411  cnfcomlem  7418  cnfcom3lem  7422  cnfcom3  7423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-suc 4414  df-1o 6495
  Copyright terms: Public domain W3C validator