Axiom ax-bdsetind 14003

Description: Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)

Hypothesis

Ref	Expression
ax-bdsetind.bd	|- BOUNDED ph

Assertion

Ref	Expression
ax-bdsetind	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )

Distinct variable groups:   y, a   ph, y

Allowed substitution hint:   ph( a)

Detailed syntax breakdown of Axiom ax-bdsetind

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff ph
2		va	. . . . . 6 setvar a
3		vy	. . . . . 6 setvar y
4	1, 2, 3	wsb 1755	. . . . 5 wff [ y / a ] ph
5	2	cv 1347	. . . . 5 class a
6	4, 3, 5	wral 2448	. . . 4 wff A. y e. a [ y / a ] ph
7	6, 1	wi 4	. . 3 wff ( A. y e. a [ y / a ] ph -> ph )
8	7, 2	wal 1346	. 2 wff A. a ( A. y e. a [ y / a ] ph -> ph )
9	1, 2	wal 1346	. 2 wff A. a ph
10	8, 9	wi 4	1 wff ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )

This axiom is referenced by:  bdsetindis  14004