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

Theorem dif1o 7189
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 7181 . . . 4  |-  1o  =  { (/) }
21difeq2i 3560 . . 3  |-  ( B 
\  1o )  =  ( B  \  { (/)
} )
32eleq2i 2482 . 2  |-  ( A  e.  ( B  \  1o )  <->  A  e.  ( B  \  { (/) } ) )
4 eldifsn 4099 . 2  |-  ( A  e.  ( B  \  { (/) } )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
53, 4bitri 251 1  |-  ( A  e.  ( B  \  1o )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 186    /\ wa 369    e. wcel 1844    =/= wne 2600    \ cdif 3413   (/)c0 3740   {csn 3974   1oc1o 7162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-nul 3741  df-sn 3975  df-suc 5418  df-1o 7169
This theorem is referenced by:  ondif1  7190  brwitnlem  7196  oelim2  7283  oeeulem  7289  oeeui  7290  omabs  7335  cantnfp1lem3  8133  cantnfp1  8134  cantnflem1  8142  cantnflem3  8144  cantnflem4  8145  cantnfleOLD  8154  cantnfp1lem2OLD  8158  cantnfp1lem3OLD  8159  cantnfp1OLD  8160  cantnflem1aOLD  8161  cantnflem1cOLD  8163  cantnflem1OLD  8165  cantnflem3OLD  8166  cantnflem4OLD  8167  cantnfOLD  8168  cnfcom3lem  8181  cnfcomlemOLD  8185  cnfcom3lemOLD  8189  cnfcom3OLD  8190
  Copyright terms: Public domain W3C validator