Theorem abbii

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

	Ref	Expression
Hypothesis	abbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	abbii	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		abbii.1	$$⊢\phi \leftrightarrow \psi$$
2		abbi1	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left\{x|\phi \right\}=\left\{x|\psi \right\}$$
3	2 1	mpg	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}$$