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

Theorem dif1o 6746
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 6738 . . . 4  |-  1o  =  { (/) }
21difeq2i 3464 . . 3  |-  ( B 
\  1o )  =  ( B  \  { (/)
} )
32eleq2i 2502 . 2  |-  ( A  e.  ( B  \  1o )  <->  A  e.  ( B  \  { (/) } ) )
4 eldifsn 3929 . 2  |-  ( A  e.  ( B  \  { (/) } )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
53, 4bitri 242 1  |-  ( A  e.  ( B  \  1o )  <->  ( A  e.  B  /\  A  =/=  (/) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1726    =/= wne 2601    \ cdif 3319   (/)c0 3630   {csn 3816   1oc1o 6719
This theorem is referenced by:  ondif1  6747  brwitnlem  6753  oelim2  6840  oeeulem  6846  oeeui  6847  omabs  6892  cantnfle  7628  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnfp1  7639  oemapvali  7642  cantnflem1a  7643  cantnflem1c  7645  cantnflem1  7647  cantnflem3  7649  cantnflem4  7650  cantnf  7651  cnfcomlem  7658  cnfcom3lem  7662  cnfcom3  7663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-ral 2712  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-nul 3631  df-sn 3822  df-suc 4589  df-1o 6726
  Copyright terms: Public domain W3C validator