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

Metamath Proof Explorer

Theorem eleq12d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994)

	Ref	Expression
Hypotheses	eleq12d.1	$⊢ φ \to A = B$
	eleq12d.2	$⊢ φ \to C = D$
Assertion	eleq12d	$⊢ φ \to (A \in C \leftrightarrow B \in D)$

Step	Hyp	Ref	Expression
1		eleq12d.1	$⊢ φ \to A = B$
2		eleq12d.2	$⊢ φ \to C = D$
3	2	eleq2d	$⊢ φ \to (A \in C \leftrightarrow A \in D)$
4	1	eleq1d	$⊢ φ \to (A \in D \leftrightarrow B \in D)$
5	3 4	bitrd	$⊢ φ \to (A \in C \leftrightarrow B \in D)$