Theorem abeq2w

Description: Version of abeq2 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024)

	Ref	Expression
Hypothesis	abeq2w.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	abeq2w	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall y\left(y\in A\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abeq2w.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		dfcleq	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in \left\{x|\phi \right\}\right)$$
3		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
4	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
5	3 4	bitri	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \psi$$
6	5	bibi2i	$$⊢\left(y\in A\leftrightarrow y\in \left\{x|\phi \right\}\right)\leftrightarrow \left(y\in A\leftrightarrow \psi \right)$$
7	6	albii	$$⊢\forall y\left(y\in A\leftrightarrow y\in \left\{x|\phi \right\}\right)\leftrightarrow \forall y\left(y\in A\leftrightarrow \psi \right)$$
8	2 7	bitri	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall y\left(y\in A\leftrightarrow \psi \right)$$