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

Metamath Proof Explorer

Theorem bj-nfext

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

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

Proof

Step Hyp Ref Expression
1 nf5 ⊢ Ⅎ y φ ↔ ∀ y φ → ∀ y φ
2 1 biimpi ⊢ Ⅎ y φ → ∀ y φ → ∀ y φ
3 2 alimi ⊢ ∀ x Ⅎ y φ → ∀ x ∀ y φ → ∀ y φ
4 nfa2 ⊢ Ⅎ y ∀ x ∀ y φ → ∀ y φ
5 bj-hbext ⊢ ∀ x ∀ y φ → ∀ y φ → ∃ x φ → ∀ y ∃ x φ
6 4 5 alrimi ⊢ ∀ x ∀ y φ → ∀ y φ → ∀ y ∃ x φ → ∀ y ∃ x φ
7 3 6 syl ⊢ ∀ x Ⅎ y φ → ∀ y ∃ x φ → ∀ y ∃ x φ
8 nf5 ⊢ Ⅎ y ∃ x φ ↔ ∀ y ∃ x φ → ∀ y ∃ x φ
9 7 8 sylibr ⊢ ∀ x Ⅎ y φ → Ⅎ y ∃ x φ