Axiom ax-coll 4120

Description: Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4174 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.)

Hypothesis

Ref	Expression
ax-coll.1	|- F/ b ph

Assertion

Ref	Expression
ax-coll	|- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )

Distinct variable group:   x, y, a, b

Allowed substitution hints:   ph( x, y, a, b)

Detailed syntax breakdown of Axiom ax-coll

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		vy	. . . 4 setvar y
3	1, 2	wex 1492	. . 3 wff E. y ph
4		vx	. . 3 setvar x
5		va	. . . 4 setvar a
6	5	cv 1352	. . 3 class a
7	3, 4, 6	wral 2455	. 2 wff A. x e. a E. y ph
8		vb	. . . . . 6 setvar b
9	8	cv 1352	. . . . 5 class b
10	1, 2, 9	wrex 2456	. . . 4 wff E. y e. b ph
11	10, 4, 6	wral 2455	. . 3 wff A. x e. a E. y e. b ph
12	11, 8	wex 1492	. 2 wff E. b A. x e. a E. y e. b ph
13	7, 12	wi 4	1 wff ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )

This axiom is referenced by:  repizf  4121  bnd  4174