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\in \left(B\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in B\wedge A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2	1	difeq2i	$$⊢B\setminus 1_{𝑜}=B\setminus \left\{\varnothing \right\}$$
3	2	eleq2i	$$⊢A\in \left(B\setminus 1_{𝑜}\right)\leftrightarrow A\in \left(B\setminus \left\{\varnothing \right\}\right)$$
4		eldifsn	$$⊢A\in \left(B\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(A\in B\wedge A\ne \varnothing \right)$$
5	3 4	bitri	$$⊢A\in \left(B\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in B\wedge A\ne \varnothing \right)$$