Theorem ralbi

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi . (Contributed by NM, 6-Oct-2003) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023)

	Ref	Expression
Assertion	ralbi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\in A\phi \leftrightarrow \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		biimp	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\phi \to \psi \right)$$
2	1	ral2imi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\in A\phi \to \forall x\in A\psi \right)$$
3		biimpr	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\psi \to \phi \right)$$
4	3	ral2imi	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\in A\psi \to \forall x\in A\phi \right)$$
5	2 4	impbid	$$⊢\forall x\in A\left(\phi \leftrightarrow \psi \right)\to \left(\forall x\in A\phi \leftrightarrow \forall x\in A\psi \right)$$