Theorem abeqabi

Description: Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024)

	Ref	Expression
Hypothesis	abeqabi.a	$$⊢A=\left\{x|\psi \right\}$$
Assertion	abeqabi	$$⊢\left\{x|\phi \right\}=A\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abeqabi.a	$$⊢A=\left\{x|\psi \right\}$$
2	1	eqeq2i	$$⊢\left\{x|\phi \right\}=A\leftrightarrow \left\{x|\phi \right\}=\left\{x|\psi \right\}$$
3		abbib	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$
4	2 3	bitri	$$⊢\left\{x|\phi \right\}=A\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$