This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-hbext

Description: Closed form of hbex . (Contributed by BJ, 10-Oct-2019)

Ref Expression
Assertion bj-hbext ⊢ ∀ y ∀ x φ → ∀ x φ → ∃ y φ → ∀ x ∃ y φ

Proof

Step Hyp Ref Expression
1 nfa2 ⊢ Ⅎ x ∀ y ∀ x φ → ∀ x φ
2 hbnt ⊢ ∀ x φ → ∀ x φ → ¬ φ → ∀ x ¬ φ
3 2 alimi ⊢ ∀ y ∀ x φ → ∀ x φ → ∀ y ¬ φ → ∀ x ¬ φ
4 bj-hbalt ⊢ ∀ y ¬ φ → ∀ x ¬ φ → ∀ y ¬ φ → ∀ x ∀ y ¬ φ
5 3 4 syl ⊢ ∀ y ∀ x φ → ∀ x φ → ∀ y ¬ φ → ∀ x ∀ y ¬ φ
6 1 5 alrimi ⊢ ∀ y ∀ x φ → ∀ x φ → ∀ x ∀ y ¬ φ → ∀ x ∀ y ¬ φ
7 hbnt ⊢ ∀ x ∀ y ¬ φ → ∀ x ∀ y ¬ φ → ¬ ∀ y ¬ φ → ∀ x ¬ ∀ y ¬ φ
8 6 7 syl ⊢ ∀ y ∀ x φ → ∀ x φ → ¬ ∀ y ¬ φ → ∀ x ¬ ∀ y ¬ φ
9 df-ex ⊢ ∃ y φ ↔ ¬ ∀ y ¬ φ
10 9 bicomi ⊢ ¬ ∀ y ¬ φ ↔ ∃ y φ
11 10 albii ⊢ ∀ x ¬ ∀ y ¬ φ ↔ ∀ x ∃ y φ
12 8 10 11 3imtr3g ⊢ ∀ y ∀ x φ → ∀ x φ → ∃ y φ → ∀ x ∃ y φ