Theorem el1o

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

	Ref	Expression
Assertion	el1o	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	eleq2i	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 ∈ { ∅ } )
3		0ex	⊢ ∅ ∈ V
4	3	elsn2	⊢ ( 𝐴 ∈ { ∅ } ↔ 𝐴 = ∅ )
5	2 4	bitri	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ )