Theorem rabbidaOLD

Description: Obsolete version of rabbida as of 14-Mar-2025. (Contributed by BJ, 27-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rabbidaOLD.n	|- F/ x ph
	rabbidaOLD.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
Assertion	rabbidaOLD	|- ( ph -> { x e. A | ps } = { x e. A | ch } )

Proof

Step	Hyp	Ref	Expression
1		rabbidaOLD.n	|- F/ x ph
2		rabbidaOLD.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ex	|- ( ph -> ( x e. A -> ( ps <-> ch ) ) )
4	1 3	ralrimi	|- ( ph -> A. x e. A ( ps <-> ch ) )
5		rabbi	|- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
6	4 5	sylib	|- ( ph -> { x e. A | ps } = { x e. A | ch } )