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

Step	Hyp	Ref	Expression
1		df1o2 7032	. . . 4 |- 1o = { (/) }
2	1	difeq2i 3569	. . 3 |- ( B \ 1o ) = ( B \ { (/) } )
3	2	eleq2i 2529	. 2 |- ( A e. ( B \ 1o ) <-> A e. ( B \ { (/) } ) )
4		eldifsn 4098	. 2 |- ( A e. ( B \ { (/) } ) <-> ( A e. B /\ A =/= (/) ) )
5	3, 4	bitri 249	1 |- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) )

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