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	⊢ ( 𝐴 ∈ ( 𝐵 ∖ 1o ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	difeq2i	⊢ ( 𝐵 ∖ 1o ) = ( 𝐵 ∖ { ∅ } )
3	2	eleq2i	⊢ ( 𝐴 ∈ ( 𝐵 ∖ 1o ) ↔ 𝐴 ∈ ( 𝐵 ∖ { ∅ } ) )
4		eldifsn	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { ∅ } ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) )
5	3 4	bitri	⊢ ( 𝐴 ∈ ( 𝐵 ∖ 1o ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) )