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

Step	Hyp	Ref	Expression
1		df1o2 7181	. . . 4 |- 1o = { (/) }
2	1	difeq2i 3560	. . 3 |- ( B \ 1o ) = ( B \ { (/) } )
3	2	eleq2i 2482	. 2 |- ( A e. ( B \ 1o ) <-> A e. ( B \ { (/) } ) )
4		eldifsn 4099	. 2 |- ( A e. ( B \ { (/) } ) <-> ( A e. B /\ A =/= (/) ) )
5	3, 4	bitri 251	1 |- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) )

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