Theorem eleq2w

Description: Weaker version of eleq2 (but more general than elequ2 ) not depending on ax-ext nor df-cleq . (Contributed by BJ, 29-Sep-2019)

	Ref	Expression
Assertion	eleq2w	$$⊢x=y\to \left(A\in x\leftrightarrow A\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		elequ2	$$⊢x=y\to \left(z\in x\leftrightarrow z\in y\right)$$
2	1	anbi2d	$$⊢x=y\to \left(\left(z=A\wedge z\in x\right)\leftrightarrow \left(z=A\wedge z\in y\right)\right)$$
3	2	exbidv	$$⊢x=y\to \left(\exists z\left(z=A\wedge z\in x\right)\leftrightarrow \exists z\left(z=A\wedge z\in y\right)\right)$$
4		dfclel	$$⊢A\in x\leftrightarrow \exists z\left(z=A\wedge z\in x\right)$$
5		dfclel	$$⊢A\in y\leftrightarrow \exists z\left(z=A\wedge z\in y\right)$$
6	3 4 5	3bitr4g	$$⊢x=y\to \left(A\in x\leftrightarrow A\in y\right)$$