Metamath Proof Explorer

Theorem eqbrb

Description: Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024)

Ref Expression
Assertion eqbrb ⊢ A = B ∧ A R C ↔ A = B ∧ B R C

Proof

Step Hyp Ref Expression
1 simpl ⊢ B = A ∧ A R C → B = A
2 eqbrtr ⊢ B = A ∧ A R C → B R C
3 1 2 jca ⊢ B = A ∧ A R C → B = A ∧ B R C
4 eqcom ⊢ B = A ↔ A = B
5 4 anbi1i ⊢ B = A ∧ A R C ↔ A = B ∧ A R C
6 4 anbi1i ⊢ B = A ∧ B R C ↔ A = B ∧ B R C
7 3 5 6 3imtr3i ⊢ A = B ∧ A R C → A = B ∧ B R C
8 simpl ⊢ A = B ∧ B R C → A = B
9 eqbrtr ⊢ A = B ∧ B R C → A R C
10 8 9 jca ⊢ A = B ∧ B R C → A = B ∧ A R C
11 7 10 impbii ⊢ A = B ∧ A R C ↔ A = B ∧ B R C