Metamath Proof Explorer

Theorem hbexg

Description: Closed form of nfex . Derived from hbexgVD . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 12-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbexg ⊢ ∀ x ∀ y φ → ∀ x φ → ∀ x ∀ y ∃ y φ → ∀ x ∃ y φ

Proof

Step Hyp Ref Expression
1 nfa2 ⊢ Ⅎ y ∀ x ∀ y φ → ∀ x φ
2 sp ⊢ ∀ y φ → ∀ x φ → φ → ∀ x φ
3 2 alimi ⊢ ∀ x ∀ y φ → ∀ x φ → ∀ x φ → ∀ x φ
4 nf5 ⊢ Ⅎ x φ ↔ ∀ x φ → ∀ x φ
5 3 4 sylibr ⊢ ∀ x ∀ y φ → ∀ x φ → Ⅎ x φ
6 1 5 nfexd ⊢ ∀ x ∀ y φ → ∀ x φ → Ⅎ x ∃ y φ
7 nf5 ⊢ Ⅎ x ∃ y φ ↔ ∀ x ∃ y φ → ∀ x ∃ y φ
8 6 7 sylib ⊢ ∀ x ∀ y φ → ∀ x φ → ∀ x ∃ y φ → ∀ x ∃ y φ
9 1 8 alrimi ⊢ ∀ x ∀ y φ → ∀ x φ → ∀ y ∀ x ∃ y φ → ∀ x ∃ y φ
10 alcom ⊢ ∀ y ∀ x ∃ y φ → ∀ x ∃ y φ ↔ ∀ x ∀ y ∃ y φ → ∀ x ∃ y φ
11 9 10 sylib ⊢ ∀ x ∀ y φ → ∀ x φ → ∀ x ∀ y ∃ y φ → ∀ x ∃ y φ