Axiom ax-strcoll 10777

Description: Axiom scheme of strong 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-strcoll	⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑥,𝑦   𝜑,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-strcoll

Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff 𝜑
2		vy	. . . . 5 setvar 𝑦
3	1, 2	wex 1421	. . . 4 wff ∃𝑦𝜑
4		vx	. . . 4 setvar 𝑥
5		va	. . . . 5 setvar 𝑎
6	5	cv 1283	. . . 4 class 𝑎
7	3, 4, 6	wral 2348	. . 3 wff ∀𝑥 ∈ 𝑎 ∃𝑦𝜑
8		vb	. . . . . . 7 setvar 𝑏
9	2, 8	wel 1434	. . . . . 6 wff 𝑦 ∈ 𝑏
10	1, 4, 6	wrex 2349	. . . . . 6 wff ∃𝑥 ∈ 𝑎 𝜑
11	9, 10	wb 103	. . . . 5 wff (𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)
12	11, 2	wal 1282	. . . 4 wff ∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)
13	12, 8	wex 1421	. . 3 wff ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)
14	7, 13	wi 4	. 2 wff (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))
15	14, 5	wal 1282	1 wff ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))

This axiom is referenced by:  strcoll2  10778