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