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