Theorem abbibw

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

	Ref	Expression
Hypotheses	abbibw.ph	$$⊢x=y\to \left(\phi \leftrightarrow \theta \right)$$
	abbibw.ps	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	abbibw	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abbibw.ph	$$⊢x=y\to \left(\phi \leftrightarrow \theta \right)$$
2		abbibw.ps	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
3		dfcleq	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\psi \right\}\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4 1	elab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \theta$$
6	4 2	elab	$$⊢y\in \left\{x|\psi \right\}\leftrightarrow \chi$$
7	5 6	bibi12i	$$⊢\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\psi \right\}\right)\leftrightarrow \left(\theta \leftrightarrow \chi \right)$$
8	7	albii	$$⊢\forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\psi \right\}\right)\leftrightarrow \forall y\left(\theta \leftrightarrow \chi \right)$$
9	1 2	bibi12d	$$⊢x=y\to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\theta \leftrightarrow \chi \right)\right)$$
10	9	bicomd	$$⊢x=y\to \left(\left(\theta \leftrightarrow \chi \right)\leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$
11	10	equcoms	$$⊢y=x\to \left(\left(\theta \leftrightarrow \chi \right)\leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$
12	11	cbvalvw	$$⊢\forall y\left(\theta \leftrightarrow \chi \right)\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$
13	3 8 12	3bitri	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$