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	$$⊢Ⅎx\phi$$
	rabbid.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	rabbid	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in A|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabbid.n	$$⊢Ⅎx\phi$$
2		rabbid.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
3	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \leftrightarrow \chi \right)$$
4	1 3	rabbida	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in A|\chi \right\}$$