Metamath Proof Explorer


Theorem bj-nfext

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

Ref Expression
Assertion bj-nfext ( ∀ 𝑥𝑦 𝜑 → Ⅎ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 nf5 ( Ⅎ 𝑦 𝜑 ↔ ∀ 𝑦 ( 𝜑 → ∀ 𝑦 𝜑 ) )
2 1 biimpi ( Ⅎ 𝑦 𝜑 → ∀ 𝑦 ( 𝜑 → ∀ 𝑦 𝜑 ) )
3 2 alimi ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑥𝑦 ( 𝜑 → ∀ 𝑦 𝜑 ) )
4 nfa2 𝑦𝑥𝑦 ( 𝜑 → ∀ 𝑦 𝜑 )
5 bj-hbext ( ∀ 𝑥𝑦 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) )
6 4 5 alrimi ( ∀ 𝑥𝑦 ( 𝜑 → ∀ 𝑦 𝜑 ) → ∀ 𝑦 ( ∃ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) )
7 3 6 syl ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦 ( ∃ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) )
8 nf5 ( Ⅎ 𝑦𝑥 𝜑 ↔ ∀ 𝑦 ( ∃ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) )
9 7 8 sylibr ( ∀ 𝑥𝑦 𝜑 → Ⅎ 𝑦𝑥 𝜑 )