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	|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph <-> A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
2	1	ral2imi	|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph -> A. x e. A ps ) )
3		biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )
4	3	ral2imi	|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ps -> A. x e. A ph ) )
5	2 4	impbid	|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph <-> A. x e. A ps ) )