Description: A key property of existential quantification (intuitionistic logic axiom ax-ie2). (Contributed by Jim Kingdon, 31-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | axie2 | ⊢ ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nf5 | ⊢ ( Ⅎ 𝑥 𝜓 ↔ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) | |
2 | 19.23t | ⊢ ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) ) | |
3 | 1 2 | sylbir | ⊢ ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) ) |