Theorem eleq1d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993) Allow shortening of eleq1 . (Revised by Wolf Lammen, 20-Nov-2019)

	Ref	Expression
Hypothesis	eleq1d.1	$$⊢\phi \to A=B$$
Assertion	eleq1d	$$⊢\phi \to \left(A\in C\leftrightarrow B\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1d.1	$$⊢\phi \to A=B$$
2	1	eqeq2d	$$⊢\phi \to \left(x=A\leftrightarrow x=B\right)$$
3	2	anbi1d	$$⊢\phi \to \left(\left(x=A\wedge x\in C\right)\leftrightarrow \left(x=B\wedge x\in C\right)\right)$$
4	3	exbidv	$$⊢\phi \to \left(\exists x\left(x=A\wedge x\in C\right)\leftrightarrow \exists x\left(x=B\wedge x\in C\right)\right)$$
5		dfclel	$$⊢A\in C\leftrightarrow \exists x\left(x=A\wedge x\in C\right)$$
6		dfclel	$$⊢B\in C\leftrightarrow \exists x\left(x=B\wedge x\in C\right)$$
7	4 5 6	3bitr4g	$$⊢\phi \to \left(A\in C\leftrightarrow B\in C\right)$$