eqelb

Description: Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019)

		Ref	Expression
	Assertion	eqelb	$⊢ (A = B \land A \in C) \leftrightarrow (A = B \land B \in C)$

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

Metamath Proof Explorer