Theorem raleqbid

Description: Equality deduction for restricted universal quantifier. See raleqbidv for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		raleqbid.0	$$⊢Ⅎx\phi$$
2		raleqbid.1	$$⊢\underset{\_}{Ⅎ}xA$$
3		raleqbid.2	$$⊢\underset{\_}{Ⅎ}xB$$
4		raleqbid.3	$$⊢\phi \to A=B$$
5		raleqbid.4	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
6	2 3	raleqf	$$⊢A=B\to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$
7	4 6	syl	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$
8	1 5	ralbid	$$⊢\phi \to \left(\forall x\in B\psi \leftrightarrow \forall x\in B\chi \right)$$
9	7 8	bitrd	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\chi \right)$$