Theorem rabbid

Description: Version of rabbidv with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rabbid.n	|- F/ x ph
2		rabbid.1	|- ( ph -> ( ps <-> ch ) )
3	2	adantr	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
4	1 3	rabbida	|- ( ph -> { x e. A | ps } = { x e. A | ch } )