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	⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )

Proof

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