Description: Version of bj-hbxfrbi with existential quantifiers. (Contributed by BJ, 23-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-hbyfrbi | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ↔ ( ∃ 𝑥 𝜓 → 𝜓 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbi | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) ) | |
2 | 1 | adantl | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) ) |
3 | simpl | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ↔ 𝜓 ) ) | |
4 | 2 3 | imbi12d | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ↔ ( ∃ 𝑥 𝜓 → 𝜓 ) ) ) |