This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ) )