Theorem rabbiiaOLD

Description: Obsolete version of rabbiia as of 12-Jan-2025. (Contributed by NM, 22-May-1999) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rabbiia.1	|- ( x e. A -> ( ph <-> ps ) )
Assertion	rabbiiaOLD	|- { 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 }