Axiom ax-setind 4220

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. (Contributed by Jim Kingdon, 19-Oct-2018.)

Assertion

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

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 1642	. . . . 5 wff [y / a]ph
5	2	cv 1241	. . . . 5 class a
6	4, 3, 5	wral 2300	. . . 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 1240	. 2 wff A. a(A.y e. a [y / a]ph -> ph)
9	1, 2	wal 1240	. 2 wff A. aph
10	8, 9	wi 4	1 wff (A. a(A.y e. a [y / a]ph -> ph) -> A. aph)

This axiom is referenced by:  setindel  4221  elirr  4224  en2lp  4232  tfi  4248  setindft  9425  setindis  9427