Axiom ax-coll 4148

Description: Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4205 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 1506	. . 3 wff E. y ph
4		vx	. . 3 setvar x
5		va	. . . 4 setvar a
6	5	cv 1363	. . 3 class a
7	3, 4, 6	wral 2475	. 2 wff A. x e. a E. y ph
8		vb	. . . . . 6 setvar b
9	8	cv 1363	. . . . 5 class b
10	1, 2, 9	wrex 2476	. . . 4 wff E. y e. b ph
11	10, 4, 6	wral 2475	. . 3 wff A. x e. a E. y e. b ph
12	11, 8	wex 1506	. 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  4149  bnd  4205