eqbrb

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

		Ref	Expression
	Assertion	eqbrb	$⊢ (A = B \land A R C) \leftrightarrow (A = B \land B R C)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (B = A \land A R C) \to B = A$
2		eqbrtr	$⊢ (B = A \land A R C) \to B R C$
3	1 2	jca	$⊢ (B = A \land A R C) \to (B = A \land B R C)$
4		eqcom	$⊢ B = A \leftrightarrow A = B$
5	4	anbi1i	$⊢ (B = A \land A R C) \leftrightarrow (A = B \land A R C)$
6	4	anbi1i	$⊢ (B = A \land B R C) \leftrightarrow (A = B \land B R C)$
7	3 5 6	3imtr3i	$⊢ (A = B \land A R C) \to (A = B \land B R C)$
8		simpl	$⊢ (A = B \land B R C) \to A = B$
9		eqbrtr	$⊢ (A = B \land B R C) \to A R C$
10	8 9	jca	$⊢ (A = B \land B R C) \to (A = B \land A R C)$
11	7 10	impbii	$⊢ (A = B \land A R C) \leftrightarrow (A = B \land B R C)$

Metamath Proof Explorer