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	|- ( ph <-> ps )
Assertion	abbii	|- { x | ph } = { x | ps }

Proof

Step	Hyp	Ref	Expression
1		abbii.1	|- ( ph <-> ps )
2		abbi1	|- ( A. x ( ph <-> ps ) -> { x | ph } = { x | ps } )
3	2 1	mpg	|- { x | ph } = { x | ps }