Theorem euabsn2w

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

	Ref	Expression
Hypotheses	absnw.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	euabsn2w.z	$$⊢x=z\to \left(\phi \leftrightarrow \theta \right)$$
Assertion	euabsn2w	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		absnw.y	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		euabsn2w.z	$$⊢x=z\to \left(\phi \leftrightarrow \theta \right)$$
3	2 1	eu6w	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
4	2	absnw	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=y\right)$$
5	4	exbii	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
6	3 5	bitr4i	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$