This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem weeq1

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997)

Ref Expression
Assertion weeq1 ⊢ R = S → R We A ↔ S We A

Proof

Step Hyp Ref Expression
1 freq1 ⊢ R = S → R Fr A ↔ S Fr A
2 soeq1 ⊢ R = S → R Or A ↔ S Or A
3 1 2 anbi12d ⊢ R = S → R Fr A ∧ R Or A ↔ S Fr A ∧ S Or A
4 df-we ⊢ R We A ↔ R Fr A ∧ R Or A
5 df-we ⊢ S We A ↔ S Fr A ∧ S Or A
6 3 4 5 3bitr4g ⊢ R = S → R We A ↔ S We A