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

Metamath Proof Explorer

Theorem weeq2

Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994)

Ref Expression
Assertion weeq2 ⊢ A = B → R We A ↔ R We B

Proof

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