Theorem rabeq12f

Description: Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018)

	Ref	Expression
Hypotheses	rabeq12f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	rabeq12f.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	rabeq12f	$$⊢\left(A=B\wedge \forall x\in A\left(\phi \leftrightarrow \psi \right)\right)\to \left\{x\in A|\phi \right\}=\left\{x\in B|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabeq12f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		rabeq12f.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		rabbi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left\{x\in A|\phi \right\}=\left\{x\in A|\psi \right\}$$
4	3	biimpi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left\{x\in A|\phi \right\}=\left\{x\in A|\psi \right\}$$
5	1 2	rabeqf	$$⊢A=B\to \left\{x\in A|\psi \right\}=\left\{x\in B|\psi \right\}$$
6	4 5	sylan9eqr	$$⊢\left(A=B\wedge \forall x\in A\left(\phi \leftrightarrow \psi \right)\right)\to \left\{x\in A|\phi \right\}=\left\{x\in B|\psi \right\}$$