Theorem rabbida

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rabbida.n	|- F/ x ph
2		rabbida.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 } )