Description: Closed form of nfex . (Contributed by BJ, 10-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nfext | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ∃ 𝑥 𝜑 ) |
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 | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ∃ 𝑥 𝜑 ) |