Axiom ax-bdsetind 14003

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

Hypothesis

Ref	Expression
ax-bdsetind.bd	⊢ BOUNDED 𝜑

Assertion

Ref	Expression
ax-bdsetind	⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)

Distinct variable groups:   𝑦,𝑎   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑎)

Detailed syntax breakdown of Axiom ax-bdsetind

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff 𝜑
2		va	. . . . . 6 setvar 𝑎
3		vy	. . . . . 6 setvar 𝑦
4	1, 2, 3	wsb 1755	. . . . 5 wff [𝑦 / 𝑎]𝜑
5	2	cv 1347	. . . . 5 class 𝑎
6	4, 3, 5	wral 2448	. . . 4 wff ∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑
7	6, 1	wi 4	. . 3 wff (∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑)
8	7, 2	wal 1346	. 2 wff ∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑)
9	1, 2	wal 1346	. 2 wff ∀𝑎𝜑
10	8, 9	wi 4	1 wff (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)

This axiom is referenced by:  bdsetindis  14004