Theorem eleq2i

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

	Ref	Expression
Hypothesis	eleq1i.1	$$⊢A=B$$
Assertion	eleq2i	$$⊢C\in A\leftrightarrow C\in B$$

Proof

Step	Hyp	Ref	Expression
1		eleq1i.1	$$⊢A=B$$
2		eleq2	$$⊢A=B\to \left(C\in A\leftrightarrow C\in B\right)$$
3	1 2	ax-mp	$$⊢C\in A\leftrightarrow C\in B$$