Axiom ax-sscoll 13185

Description: Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
ax-sscoll	⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧   𝜑,𝑎,𝑏,𝑐,𝑑

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Axiom ax-sscoll

Step	Hyp	Ref	Expression
1		wph	. . . . . . . 8 wff 𝜑
2		vy	. . . . . . . 8 setvar 𝑦
3		vb	. . . . . . . . 9 setvar 𝑏
4	3	cv 1330	. . . . . . . 8 class 𝑏
5	1, 2, 4	wrex 2417	. . . . . . 7 wff ∃𝑦 ∈ 𝑏 𝜑
6		vx	. . . . . . 7 setvar 𝑥
7		va	. . . . . . . 8 setvar 𝑎
8	7	cv 1330	. . . . . . 7 class 𝑎
9	5, 6, 8	wral 2416	. . . . . 6 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑
10		vd	. . . . . . . . . 10 setvar 𝑑
11	2, 10	wel 1481	. . . . . . . . 9 wff 𝑦 ∈ 𝑑
12	1, 6, 8	wrex 2417	. . . . . . . . 9 wff ∃𝑥 ∈ 𝑎 𝜑
13	11, 12	wb 104	. . . . . . . 8 wff (𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)
14	13, 2	wal 1329	. . . . . . 7 wff ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)
15		vc	. . . . . . . 8 setvar 𝑐
16	15	cv 1330	. . . . . . 7 class 𝑐
17	14, 10, 16	wrex 2417	. . . . . 6 wff ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)
18	9, 17	wi 4	. . . . 5 wff (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
19		vz	. . . . 5 setvar 𝑧
20	18, 19	wal 1329	. . . 4 wff ∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
21	20, 15	wex 1468	. . 3 wff ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
22	21, 3	wal 1329	. 2 wff ∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
23	22, 7	wal 1329	1 wff ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))

This axiom is referenced by:  sscoll2  13186