Metamath Proof Explorer


Theorem ereq2

Description: Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion ereq2 ( 𝐴 = 𝐵 → ( 𝑅 Er 𝐴𝑅 Er 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ( 𝐴 = 𝐵 → ( dom 𝑅 = 𝐴 ↔ dom 𝑅 = 𝐵 ) )
2 1 3anbi2d ( 𝐴 = 𝐵 → ( ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( 𝑅 ∪ ( 𝑅𝑅 ) ) ⊆ 𝑅 ) ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐵 ∧ ( 𝑅 ∪ ( 𝑅𝑅 ) ) ⊆ 𝑅 ) ) )
3 df-er ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( 𝑅 ∪ ( 𝑅𝑅 ) ) ⊆ 𝑅 ) )
4 df-er ( 𝑅 Er 𝐵 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐵 ∧ ( 𝑅 ∪ ( 𝑅𝑅 ) ) ⊆ 𝑅 ) )
5 2 3 4 3bitr4g ( 𝐴 = 𝐵 → ( 𝑅 Er 𝐴𝑅 Er 𝐵 ) )