Axiom ax-setind 4513

Description: Axiom of e.-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	|- ( 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-setind

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff ph
2		va	. . . . . 6 setvar a
3		vy	. . . . . 6 setvar y
4	1, 2, 3	wsb 1750	. . . . 5 wff [ y / a ] ph
5	2	cv 1342	. . . . 5 class a
6	4, 3, 5	wral 2443	. . . 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 1341	. 2 wff A. a ( A. y e. a [ y / a ] ph -> ph )
9	1, 2	wal 1341	. 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:  setindel  4514  elirr  4517  en2lp  4530  zfregfr  4550  tfi  4558  setindft  13807  setindis  13809