Theorem rabbiia

Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999) (Proof shortened by Wolf Lammen, 12-Jan-2025)

	Ref	Expression
Hypothesis	rabbiia.1	|- ( x e. A -> ( ph <-> ps ) )
Assertion	rabbiia	|- { x e. A | ph } = { x e. A | ps }

Proof

Step	Hyp	Ref	Expression
1		rabbiia.1	|- ( x e. A -> ( ph <-> ps ) )
2	1	pm5.32i	|- ( ( x e. A /\ ph ) <-> ( x e. A /\ ps ) )
3	2	rabbia2	|- { x e. A | ph } = { x e. A | ps }