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

Proof

Step	Hyp	Ref	Expression
1		abeqabi.a	|- A = { x | ps }
2	1	eqeq2i	|- ( { x | ph } = A <-> { x | ph } = { x | ps } )
3		abbib	|- ( { x | ph } = { x | ps } <-> A. x ( ph <-> ps ) )
4	2 3	bitri	|- ( { x | ph } = A <-> A. x ( ph <-> ps ) )