Metamath Proof Explorer

Theorem eqbrtr

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

Ref Expression
Assertion eqbrtr 
|- ( ( A = B /\ B R C ) -> A R C )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( A = B -> ( A R C <-> B R C ) )
2 1 biimpar 
 |-  ( ( A = B /\ B R C ) -> A R C )