Theorem absnw

Description: Replace ax-10 , ax-11 , ax-12 in absn with a substitution hypothesis. (Contributed by SN, 27-May-2025)

	Ref	Expression
Hypothesis	absnw.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	absnw	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		absnw.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		df-sn	$$⊢\left\{Y\right\}=\left\{x|x=Y\right\}$$
3	2	eqeq2i	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{x|x=Y\right\}$$
4		eqeq1	$$⊢x=y\to \left(x=Y\leftrightarrow y=Y\right)$$
5	1 4	abbibw	$$⊢\left\{x|\phi \right\}=\left\{x|x=Y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=Y\right)$$
6	3 5	bitri	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=Y\right)$$