Axiom ax-ie2 1508

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

Assertion

Ref	Expression
ax-ie2	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )

Detailed syntax breakdown of Axiom ax-ie2

Step	Hyp	Ref	Expression
1		wps	. . . 4 wff ps
2		vx	. . . . 5 setvar x
3	1, 2	wal 1362	. . . 4 wff A. x ps
4	1, 3	wi 4	. . 3 wff ( ps -> A. x ps )
5	4, 2	wal 1362	. 2 wff A. x ( ps -> A. x ps )
6		wph	. . . . 5 wff ph
7	6, 1	wi 4	. . . 4 wff ( ph -> ps )
8	7, 2	wal 1362	. . 3 wff A. x ( ph -> ps )
9	6, 2	wex 1506	. . . 4 wff E. x ph
10	9, 1	wi 4	. . 3 wff ( E. x ph -> ps )
11	8, 10	wb 105	. 2 wff ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
12	5, 11	wi 4	1 wff ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )

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