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

Proof

Step	Hyp	Ref	Expression
1		rabbidaOLD.n	$$⊢Ⅎx\phi$$
2		rabbidaOLD.1	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \leftrightarrow \chi \right)$$
3	2	ex	$$⊢\phi \to \left(x\in A\to \left(\psi \leftrightarrow \chi \right)\right)$$
4	1 3	ralrimi	$$⊢\phi \to \forall x\in A\left(\psi \leftrightarrow \chi \right)$$
5		rabbi	$$⊢\forall x\in A\left(\psi \leftrightarrow \chi \right)\leftrightarrow \left\{x\in A|\psi \right\}=\left\{x\in A|\chi \right\}$$
6	4 5	sylib	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in A|\chi \right\}$$