Axiom ax-coll 3863

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

Hypothesis

Ref	Expression
ax-coll.1	⊢ Ⅎ𝑏φ

Assertion

Ref	Expression
ax-coll	⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)

Distinct variable group:   x,y,𝑎,𝑏

Allowed substitution hints:   φ(x,y,𝑎,𝑏)

Detailed syntax breakdown of Axiom ax-coll

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff φ
2		vy	. . . 4 setvar y
3	1, 2	wex 1378	. . 3 wff ∃yφ
4		vx	. . 3 setvar x
5		va	. . . 4 setvar 𝑎
6	5	cv 1241	. . 3 class 𝑎
7	3, 4, 6	wral 2300	. 2 wff ∀x ∈ 𝑎 ∃yφ
8		vb	. . . . . 6 setvar 𝑏
9	8	cv 1241	. . . . 5 class 𝑏
10	1, 2, 9	wrex 2301	. . . 4 wff ∃y ∈ 𝑏 φ
11	10, 4, 6	wral 2300	. . 3 wff ∀x ∈ 𝑎 ∃y ∈ 𝑏 φ
12	11, 8	wex 1378	. 2 wff ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ
13	7, 12	wi 4	1 wff (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)

This axiom is referenced by:  repizf  3864  bnd  3916