Theorem rexbi

Description: Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024) (Proof shortened by Wolf Lammen, 3-Nov-2024)

	Ref	Expression
Assertion	rexbi	|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
2	1	ralimi	|- ( A. x e. A ( ph <-> ps ) -> A. x e. A ( ph -> ps ) )
3		rexim	|- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
4	2 3	syl	|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
5		biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )
6	5	ralimi	|- ( A. x e. A ( ph <-> ps ) -> A. x e. A ( ps -> ph ) )
7		rexim	|- ( A. x e. A ( ps -> ph ) -> ( E. x e. A ps -> E. x e. A ph ) )
8	6 7	syl	|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ps -> E. x e. A ph ) )
9	4 8	impbid	|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )