Theorem 0ellim

Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994)

	Ref	Expression
Assertion	0ellim	⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dflim2	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) )
2	1	simp2bi	⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )