Axiom ax-ie2 1508

Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
ax-ie2	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))

Detailed syntax breakdown of Axiom ax-ie2

Step	Hyp	Ref	Expression
1		wps	. . . 4 wff 𝜓
2		vx	. . . . 5 setvar 𝑥
3	1, 2	wal 1362	. . . 4 wff ∀𝑥𝜓
4	1, 3	wi 4	. . 3 wff (𝜓 → ∀𝑥𝜓)
5	4, 2	wal 1362	. 2 wff ∀𝑥(𝜓 → ∀𝑥𝜓)
6		wph	. . . . 5 wff 𝜑
7	6, 1	wi 4	. . . 4 wff (𝜑 → 𝜓)
8	7, 2	wal 1362	. . 3 wff ∀𝑥(𝜑 → 𝜓)
9	6, 2	wex 1506	. . . 4 wff ∃𝑥𝜑
10	9, 1	wi 4	. . 3 wff (∃𝑥𝜑 → 𝜓)
11	8, 10	wb 105	. 2 wff (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
12	5, 11	wi 4	1 wff (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))

This axiom is referenced by:  19.23ht  1511  bj-ex  15492