Metamath Proof Explorer


Theorem weeq1

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

Ref Expression
Assertion weeq1 ( 𝑅 = 𝑆 → ( 𝑅 We 𝐴𝑆 We 𝐴 ) )

Proof

Step Hyp Ref Expression
1 freq1 ( 𝑅 = 𝑆 → ( 𝑅 Fr 𝐴𝑆 Fr 𝐴 ) )
2 soeq1 ( 𝑅 = 𝑆 → ( 𝑅 Or 𝐴𝑆 Or 𝐴 ) )
3 1 2 anbi12d ( 𝑅 = 𝑆 → ( ( 𝑅 Fr 𝐴𝑅 Or 𝐴 ) ↔ ( 𝑆 Fr 𝐴𝑆 Or 𝐴 ) ) )
4 df-we ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴𝑅 Or 𝐴 ) )
5 df-we ( 𝑆 We 𝐴 ↔ ( 𝑆 Fr 𝐴𝑆 Or 𝐴 ) )
6 3 4 5 3bitr4g ( 𝑅 = 𝑆 → ( 𝑅 We 𝐴𝑆 We 𝐴 ) )