Theorem eqab

Description: One direction of eqabb is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025)

	Ref	Expression
Assertion	eqab	$$⊢\forall x\left(x\in A\leftrightarrow \phi \right)\to A=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		abid1	$$⊢A=\left\{x|x\in A\right\}$$
2		abbi	$$⊢\forall x\left(x\in A\leftrightarrow \phi \right)\to \left\{x|x\in A\right\}=\left\{x|\phi \right\}$$
3	1 2	eqtrid	$$⊢\forall x\left(x\in A\leftrightarrow \phi \right)\to A=\left\{x|\phi \right\}$$