Metamath Proof Explorer


Theorem weeq2

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

Ref Expression
Assertion weeq2 A=BRWeARWeB

Proof

Step Hyp Ref Expression
1 freq2 A=BRFrARFrB
2 soeq2 A=BROrAROrB
3 1 2 anbi12d A=BRFrAROrARFrBROrB
4 df-we RWeARFrAROrA
5 df-we RWeBRFrBROrB
6 3 4 5 3bitr4g A=BRWeARWeB