Theorem rexbi

Description: Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-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		ralbi	|- ( A. x e. A ( -. ph <-> -. ps ) -> ( A. x e. A -. ph <-> A. x e. A -. ps ) )
2	1	notbid	|- ( A. x e. A ( -. ph <-> -. ps ) -> ( -. A. x e. A -. ph <-> -. A. x e. A -. ps ) )
3		notbi	|- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
4	3	ralbii	|- ( A. x e. A ( ph <-> ps ) <-> A. x e. A ( -. ph <-> -. ps ) )
5		dfrex2	|- ( E. x e. A ph <-> -. A. x e. A -. ph )
6		dfrex2	|- ( E. x e. A ps <-> -. A. x e. A -. ps )
7	5 6	bibi12i	|- ( ( E. x e. A ph <-> E. x e. A ps ) <-> ( -. A. x e. A -. ph <-> -. A. x e. A -. ps ) )
8	2 4 7	3imtr4i	|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )