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 ) ) ) |
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 ) ) ) |