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	⊢ Ⅎ𝑏𝜑

Assertion

Ref	Expression
ax-coll	⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)

Distinct variable group:   𝑥,𝑦,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏)

Detailed syntax breakdown of Axiom ax-coll

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 setvar 𝑦
3	1, 2	wex 1506	. . 3 wff ∃𝑦𝜑
4		vx	. . 3 setvar 𝑥
5		va	. . . 4 setvar 𝑎
6	5	cv 1363	. . 3 class 𝑎
7	3, 4, 6	wral 2475	. 2 wff ∀𝑥 ∈ 𝑎 ∃𝑦𝜑
8		vb	. . . . . 6 setvar 𝑏
9	8	cv 1363	. . . . 5 class 𝑏
10	1, 2, 9	wrex 2476	. . . 4 wff ∃𝑦 ∈ 𝑏 𝜑
11	10, 4, 6	wral 2475	. . 3 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑
12	11, 8	wex 1506	. 2 wff ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑
13	7, 12	wi 4	1 wff (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)

This axiom is referenced by:  repizf  4149  bnd  4205