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

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