Axiom ax-strcoll 14017

Description: Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that ph represents a multivalued function on a, or equivalently a collection of nonempty classes indexed by a, and the axiom asserts the existence of a set b which "collects" at least one element in the image of each x e. a and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4104. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
ax-strcoll	|- A. a ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )

Distinct variable groups:   a, b, x, y   ph, a, b

Allowed substitution hints:   ph( x, y)

Detailed syntax breakdown of Axiom ax-strcoll

Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff ph
2		vy	. . . . 5 setvar y
3	1, 2	wex 1485	. . . 4 wff E. y ph
4		vx	. . . 4 setvar x
5		va	. . . . 5 setvar a
6	5	cv 1347	. . . 4 class a
7	3, 4, 6	wral 2448	. . 3 wff A. x e. a E. y ph
8		vb	. . . . . . . 8 setvar b
9	8	cv 1347	. . . . . . 7 class b
10	1, 2, 9	wrex 2449	. . . . . 6 wff E. y e. b ph
11	10, 4, 6	wral 2448	. . . . 5 wff A. x e. a E. y e. b ph
12	1, 4, 6	wrex 2449	. . . . . 6 wff E. x e. a ph
13	12, 2, 9	wral 2448	. . . . 5 wff A. y e. b E. x e. a ph
14	11, 13	wa 103	. . . 4 wff ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph )
15	14, 8	wex 1485	. . 3 wff E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph )
16	7, 15	wi 4	. 2 wff ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )
17	16, 5	wal 1346	1 wff A. a ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )

This axiom is referenced by:  strcoll2  14018