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

Theorem dif1o 7040
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 7032 . . . 4  |-  1o  =  { (/) }
21difeq2i 3569 . . 3  |-  ( B 
\  1o )  =  ( B  \  { (/)
} )
32eleq2i 2529 . 2  |-  ( A  e.  ( B  \  1o )  <->  A  e.  ( B  \  { (/) } ) )
4 eldifsn 4098 . 2  |-  ( A  e.  ( B  \  { (/) } )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
53, 4bitri 249 1  |-  ( A  e.  ( B  \  1o )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1758    =/= wne 2644    \ cdif 3423   (/)c0 3735   {csn 3975   1oc1o 7013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-nul 3736  df-sn 3976  df-suc 4823  df-1o 7020
This theorem is referenced by:  ondif1  7041  brwitnlem  7047  oelim2  7134  oeeulem  7140  oeeui  7141  omabs  7186  cantnfp1lem3  7989  cantnfp1  7990  cantnflem1  7998  cantnflem3  8000  cantnflem4  8001  cantnfleOLD  8010  cantnfp1lem2OLD  8014  cantnfp1lem3OLD  8015  cantnfp1OLD  8016  cantnflem1aOLD  8017  cantnflem1cOLD  8019  cantnflem1OLD  8021  cantnflem3OLD  8022  cantnflem4OLD  8023  cantnfOLD  8024  cnfcom3lem  8037  cnfcomlemOLD  8041  cnfcom3lemOLD  8045  cnfcom3OLD  8046
  Copyright terms: Public domain W3C validator