Axiom ax-ie2 1313

Description: Define existential quantification. ∃xφ means "there exists at least one set x such that φ is true." Axiom 10 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
ax-ie2	⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))

Detailed syntax breakdown of Axiom ax-ie2

Step	Hyp	Ref	Expression
1		wps	. . . 4 wff ψ
2		vx	. . . . 5 set x
3	1, 2	wal 1264	. . . 4 wff ∀xψ
4	1, 3	wi 4	. . 3 wff (ψ → ∀xψ)
5	4, 2	wal 1264	. 2 wff ∀x(ψ → ∀xψ)
6		wph	. . . . 5 wff φ
7	6, 1	wi 4	. . . 4 wff (φ → ψ)
8	7, 2	wal 1264	. . 3 wff ∀x(φ → ψ)
9	6, 2	wex 1311	. . . 4 wff ∃xφ
10	9, 1	wi 4	. . 3 wff (∃xφ → ψ)
11	8, 10	wb 96	. 2 wff (∀x(φ → ψ) ↔ (∃xφ → ψ))
12	5, 11	wi 4	1 wff (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))

This axiom is referenced by:  19.23t  1316