Metamath Proof Explorer

Theorem ondif1

Description: Two ways to say that A is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion ondif1 ⊢ A ∈ On ∖ 1 𝑜 ↔ A ∈ On ∧ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 dif1o ⊢ A ∈ On ∖ 1 𝑜 ↔ A ∈ On ∧ A ≠ ∅
2 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
3 2 pm5.32i ⊢ A ∈ On ∧ ∅ ∈ A ↔ A ∈ On ∧ A ≠ ∅
4 1 3 bitr4i ⊢ A ∈ On ∖ 1 𝑜 ↔ A ∈ On ∧ ∅ ∈ A