This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in (B ∖ 1_{𝑜}) \leftrightarrow (A \in B \land A \neq \emptyset)$

Step	Hyp	Ref	Expression
1		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
2	1	difeq2i	$⊢ B ∖ 1_{𝑜} = B ∖ \{\emptyset\}$
3	2	eleq2i	$⊢ A \in (B ∖ 1_{𝑜}) \leftrightarrow A \in (B ∖ \{\emptyset\})$
4		eldifsn	$⊢ A \in (B ∖ \{\emptyset\}) \leftrightarrow (A \in B \land A \neq \emptyset)$
5	3 4	bitri	$⊢ A \in (B ∖ 1_{𝑜}) \leftrightarrow (A \in B \land A \neq \emptyset)$