Metamath Proof Explorer


Theorem weeq1

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

Ref Expression
Assertion weeq1 R=SRWeASWeA

Proof

Step Hyp Ref Expression
1 freq1 R=SRFrASFrA
2 soeq1 R=SROrASOrA
3 1 2 anbi12d R=SRFrAROrASFrASOrA
4 df-we RWeARFrAROrA
5 df-we SWeASFrASOrA
6 3 4 5 3bitr4g R=SRWeASWeA