Theorem rabimbieq

Description: Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021)

	Ref	Expression
Hypotheses	rabimbieq.1	|- B = { x e. A | ph }
	rabimbieq.2	|- ( x e. A -> ( ph <-> ps ) )
Assertion	rabimbieq	|- B = { x e. A | ps }

Proof

Step	Hyp	Ref	Expression
1		rabimbieq.1	|- B = { x e. A | ph }
2		rabimbieq.2	|- ( x e. A -> ( ph <-> ps ) )
3	2	rabbiia	|- { x e. A | ph } = { x e. A | ps }
4	1 3	eqtri	|- B = { x e. A | ps }