Theorem eleq1w

Description: Weaker version of eleq1 (but more general than elequ1 ) not depending on ax-ext nor df-cleq .

Note that this provides a proof of ax-8 from Tarski's FOL and dfclel (simply consider an instance where A is replaced by a setvar and deduce the forward implication by biimpd ), which shows that dfclel is too powerful to be used as a definition instead of df-clel . (Contributed by BJ, 24-Jun-2019)

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

Proof

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