Theorem ralbi12f

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

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

Proof

Step	Hyp	Ref	Expression
1		ralbi12f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		ralbi12f.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		ralbi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\in A\phi \leftrightarrow \forall x\in A\psi \right)$$
4	1 2	raleqf	$$⊢A=B\to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$
5	3 4	sylan9bbr	$$⊢\left(A=B\wedge \forall x\in A\left(\phi \leftrightarrow \psi \right)\right)\to \left(\forall x\in A\phi \leftrightarrow \forall x\in B\psi \right)$$