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 is a nonzero number of the set . (Contributed by Mario Carneiro, 21-May-2015.)
Assertion
Ref Expression
dif1o

Proof of Theorem dif1o
StepHypRef Expression
1 df1o2 6738 . . . 4
21difeq2i 3464 . . 3
32eleq2i 2502 . 2
4 eldifsn 3929 . 2
53, 4bitri 242 1
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360   wcel 1726   wne 2601   cdif 3319  c0 3630  csn 3816  c1o 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