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) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 14-Mar-2025)

	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	pm5.32da	|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
4	1 3	rabbida4	|- ( ph -> { x e. A | ps } = { x e. A | ch } )