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

Theorem dif1o 7169
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 7161 . . . 4
21difeq2i 3618 . . 3
32eleq2i 2535 . 2
4 eldifsn 4155 . 2
53, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  =/=wne 2652  \cdif 3472   c0 3784  {csn 4029   c1o 7142
This theorem is referenced by:  ondif1  7170  brwitnlem  7176  oelim2  7263  oeeulem  7269  oeeui  7270  omabs  7315  cantnfp1lem3  8120  cantnfp1  8121  cantnflem1  8129  cantnflem3  8131  cantnflem4  8132  cantnfleOLD  8141  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1aOLD  8148  cantnflem1cOLD  8150  cantnflem1OLD  8152  cantnflem3OLD  8153  cantnflem4OLD  8154  cantnfOLD  8155  cnfcom3lem  8168  cnfcomlemOLD  8172  cnfcom3lemOLD  8176  cnfcom3OLD  8177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-sn 4030  df-suc 4889  df-1o 7149
  Copyright terms: Public domain W3C validator