Metamath Proof Explorer


Theorem bj-hbyfrbi

Description: Version of bj-hbxfrbi with existential quantifiers. (Contributed by BJ, 23-Aug-2023)

Ref Expression
Assertion bj-hbyfrbi
|- ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ( E. x ph -> ph ) <-> ( E. x ps -> ps ) ) )

Proof

Step Hyp Ref Expression
1 exbi
 |-  ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2 1 adantl
 |-  ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( E. x ph <-> E. x ps ) )
3 simpl
 |-  ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ph <-> ps ) )
4 2 3 imbi12d
 |-  ( ( ( ph <-> ps ) /\ A. x ( ph <-> ps ) ) -> ( ( E. x ph -> ph ) <-> ( E. x ps -> ps ) ) )