Axiom ax-setind 4513

Description: Axiom of ∈-Induction (also known as set induction). An axiom of Intuitionistic Zermelo-Fraenkel set theory. Axiom 9 of [Crosilla] p. "Axioms of CZF and IZF". This replaces the Axiom of Foundation (also called Regularity) from Zermelo-Fraenkel set theory.

For more on axioms which might be adopted which are incompatible with this axiom (that is, Non-wellfounded Set Theory but in the absence of excluded middle), see Chapter 20 of [AczelRathjen], p. 183. (Contributed by Jim Kingdon, 19-Oct-2018.)

Assertion

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

Distinct variable groups:   𝑦,𝑎   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑎)

Detailed syntax breakdown of Axiom ax-setind

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

This axiom is referenced by:  setindel  4514  elirr  4517  en2lp  4530  zfregfr  4550  tfi  4558  setindft  13807  setindis  13809