Theorem el1o

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

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

Proof

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