Theorem ondif1i

Description: Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of Schloeder p. 2. See ondif1 . (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	ondif1i	⊢ ( 𝐴 ∈ ( On ∖ 1o ) → ∅ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ondif1	⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
2	1	simprbi	⊢ ( 𝐴 ∈ ( On ∖ 1o ) → ∅ ∈ 𝐴 )