Theorem bj-rabeqd

Description: Deduction form of rabeq . Note that contrary to rabeq it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019)

	Ref	Expression
Hypotheses	bj-rabeqd.nf	$$⊢Ⅎx\phi$$
	bj-rabeqd.1	$$⊢\phi \to A=B$$
Assertion	bj-rabeqd	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-rabeqd.nf	$$⊢Ⅎx\phi$$
2		bj-rabeqd.1	$$⊢\phi \to A=B$$
3		eleq2	$$⊢A=B\to \left(x\in A\leftrightarrow x\in B\right)$$
4	3	anbi1d	$$⊢A=B\to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \psi \right)\right)$$
5	2 4	syl	$$⊢\phi \to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \psi \right)\right)$$
6	1 5	bj-rabbida2	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$