Metamath Proof Explorer


Theorem freq2

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

Ref Expression
Assertion freq2 A=BRFrARFrB

Proof

Step Hyp Ref Expression
1 eqimss2 A=BBA
2 frss BARFrARFrB
3 1 2 syl A=BRFrARFrB
4 eqimss A=BAB
5 frss ABRFrBRFrA
6 4 5 syl A=BRFrBRFrA
7 3 6 impbid A=BRFrARFrB