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 ( ( ( 𝜑𝜓 ) ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → ( ( ∃ 𝑥 𝜑𝜑 ) ↔ ( ∃ 𝑥 𝜓𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 exbi ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) )
2 1 adantl ( ( ( 𝜑𝜓 ) ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) )
3 simpl ( ( ( 𝜑𝜓 ) ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → ( 𝜑𝜓 ) )
4 2 3 imbi12d ( ( ( 𝜑𝜓 ) ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → ( ( ∃ 𝑥 𝜑𝜑 ) ↔ ( ∃ 𝑥 𝜓𝜓 ) ) )