Theorem eleq12i

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

	Ref	Expression
Hypotheses	eleq1i.1	$$⊢A=B$$
	eleq12i.2	$$⊢C=D$$
Assertion	eleq12i	$$⊢A\in C\leftrightarrow B\in D$$

Proof

Step	Hyp	Ref	Expression
1		eleq1i.1	$$⊢A=B$$
2		eleq12i.2	$$⊢C=D$$
3	2	eleq2i	$$⊢A\in C\leftrightarrow A\in D$$
4	1	eleq1i	$$⊢A\in D\leftrightarrow B\in D$$
5	3 4	bitri	$$⊢A\in C\leftrightarrow B\in D$$