Metamath Proof Explorer

Theorem dif1o

Description: Two ways to say that A is a nonzero number of the set B . (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion dif1o 
|- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) )

Proof

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