Theorem rabbiia

Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999)

	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	abbii	|- { x | ( x e. A /\ ph ) } = { x | ( x e. A /\ ps ) }
4		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
5		df-rab	|- { x e. A | ps } = { x | ( x e. A /\ ps ) }
6	3 4 5	3eqtr4i	|- { x e. A | ph } = { x e. A | ps }