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

Metamath Proof Explorer

Theorem ereq1

Description: Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion ereq1 ( 𝑅 = 𝑆 → ( 𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴 ) )

Proof

Step Hyp Ref Expression
1 releq ⊢ ( 𝑅 = 𝑆 → ( Rel 𝑅 ↔ Rel 𝑆 ) )
2 dmeq ⊢ ( 𝑅 = 𝑆 → dom 𝑅 = dom 𝑆 )
3 2 eqeq1d ⊢ ( 𝑅 = 𝑆 → ( dom 𝑅 = 𝐴 ↔ dom 𝑆 = 𝐴 ) )
4 cnveq ⊢ ( 𝑅 = 𝑆 → ◡ 𝑅 = ◡ 𝑆 )
5 coeq1 ⊢ ( 𝑅 = 𝑆 → ( 𝑅 ∘ 𝑅 ) = ( 𝑆 ∘ 𝑅 ) )
6 coeq2 ⊢ ( 𝑅 = 𝑆 → ( 𝑆 ∘ 𝑅 ) = ( 𝑆 ∘ 𝑆 ) )
7 5 6 eqtrd ⊢ ( 𝑅 = 𝑆 → ( 𝑅 ∘ 𝑅 ) = ( 𝑆 ∘ 𝑆 ) )
8 4 7 uneq12d ⊢ ( 𝑅 = 𝑆 → ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) = ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) )
9 8 sseq1d ⊢ ( 𝑅 = 𝑆 → ( ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ↔ ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑅 ) )
10 sseq2 ⊢ ( 𝑅 = 𝑆 → ( ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑅 ↔ ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑆 ) )
11 9 10 bitrd ⊢ ( 𝑅 = 𝑆 → ( ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ↔ ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑆 ) )
12 1 3 11 3anbi123d ⊢ ( 𝑅 = 𝑆 → ( ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) ↔ ( Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑆 ) ) )
13 df-er ⊢ ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )
14 df-er ⊢ ( 𝑆 Er 𝐴 ↔ ( Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ ( ◡ 𝑆 ∪ ( 𝑆 ∘ 𝑆 ) ) ⊆ 𝑆 ) )
15 12 13 14 3bitr4g ⊢ ( 𝑅 = 𝑆 → ( 𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴 ) )