Theorem rabeqdv

Description: Equality of restricted class abstractions. Deduction form of rabeq . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypothesis	rabeqdv.1	$$⊢\phi \to A=B$$
Assertion	rabeqdv	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabeqdv.1	$$⊢\phi \to A=B$$
2		rabeq	$$⊢A=B\to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$
3	1 2	syl	$$⊢\phi \to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$