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

Metamath Proof Explorer

Theorem el1o

Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005)

		Ref	Expression
	Assertion	el1o	$⊢ A \in 1_{𝑜} \leftrightarrow A = \emptyset$

Step	Hyp	Ref	Expression
1		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
2	1	eleq2i	$⊢ A \in 1_{𝑜} \leftrightarrow A \in \{\emptyset\}$
3		0ex	$⊢ \emptyset \in V$
4	3	elsn2	$⊢ A \in \{\emptyset\} \leftrightarrow A = \emptyset$
5	2 4	bitri	$⊢ A \in 1_{𝑜} \leftrightarrow A = \emptyset$