Metamath Proof Explorer

Theorem ordeq

Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993)

Ref Expression
Assertion ordeq ⊢ A = B → Ord ⁡ A ↔ Ord ⁡ B

Proof

Step Hyp Ref Expression
1 treq ⊢ A = B → Tr ⁡ A ↔ Tr ⁡ B
2 weeq2 ⊢ A = B → E We A ↔ E We B
3 1 2 anbi12d ⊢ A = B → Tr ⁡ A ∧ E We A ↔ Tr ⁡ B ∧ E We B
4 df-ord ⊢ Ord ⁡ A ↔ Tr ⁡ A ∧ E We A
5 df-ord ⊢ Ord ⁡ B ↔ Tr ⁡ B ∧ E We B
6 3 4 5 3bitr4g ⊢ A = B → Ord ⁡ A ↔ Ord ⁡ B