Theorem eleq12d

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

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

Proof

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