Metamath Proof Explorer


Theorem freq1

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

Ref Expression
Assertion freq1 ( 𝑅 = 𝑆 → ( 𝑅 Fr 𝐴𝑆 Fr 𝐴 ) )

Proof

Step Hyp Ref Expression
1 breq ( 𝑅 = 𝑆 → ( 𝑧 𝑅 𝑦𝑧 𝑆 𝑦 ) )
2 1 notbid ( 𝑅 = 𝑆 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑆 𝑦 ) )
3 2 rexralbidv ( 𝑅 = 𝑆 → ( ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ↔ ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑆 𝑦 ) )
4 3 imbi2d ( 𝑅 = 𝑆 → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑆 𝑦 ) ) )
5 4 albidv ( 𝑅 = 𝑆 → ( ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑆 𝑦 ) ) )
6 df-fr ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑅 𝑦 ) )
7 df-fr ( 𝑆 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ∃ 𝑦𝑥𝑧𝑥 ¬ 𝑧 𝑆 𝑦 ) )
8 5 6 7 3bitr4g ( 𝑅 = 𝑆 → ( 𝑅 Fr 𝐴𝑆 Fr 𝐴 ) )