Axiom ax-sscoll 13869

Description: Axiom scheme of subset 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 from a to b, or equivalently a collection of nonempty subsets of b indexed by a, and the consequent asserts the existence of a subset of c which "collects" at least one element in the image of each x e. a and which is made only of such elements. The axiom asserts the existence, for any sets a , b, of a set c such that that implication holds for any value of the parameter z of ph. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
ax-sscoll	|- A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )

Distinct variable groups:   a, b, c, d, x, y, z   ph, a, b, c, d

Allowed substitution hints:   ph( x, y, z)

Detailed syntax breakdown of Axiom ax-sscoll

Step	Hyp	Ref	Expression
1		wph	. . . . . . . 8 wff ph
2		vy	. . . . . . . 8 setvar y
3		vb	. . . . . . . . 9 setvar b
4	3	cv 1342	. . . . . . . 8 class b
5	1, 2, 4	wrex 2445	. . . . . . 7 wff E. y e. b ph
6		vx	. . . . . . 7 setvar x
7		va	. . . . . . . 8 setvar a
8	7	cv 1342	. . . . . . 7 class a
9	5, 6, 8	wral 2444	. . . . . 6 wff A. x e. a E. y e. b ph
10		vd	. . . . . . . . . . 11 setvar d
11	10	cv 1342	. . . . . . . . . 10 class d
12	1, 2, 11	wrex 2445	. . . . . . . . 9 wff E. y e. d ph
13	12, 6, 8	wral 2444	. . . . . . . 8 wff A. x e. a E. y e. d ph
14	1, 6, 8	wrex 2445	. . . . . . . . 9 wff E. x e. a ph
15	14, 2, 11	wral 2444	. . . . . . . 8 wff A. y e. d E. x e. a ph
16	13, 15	wa 103	. . . . . . 7 wff ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph )
17		vc	. . . . . . . 8 setvar c
18	17	cv 1342	. . . . . . 7 class c
19	16, 10, 18	wrex 2445	. . . . . 6 wff E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph )
20	9, 19	wi 4	. . . . 5 wff ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
21		vz	. . . . 5 setvar z
22	20, 21	wal 1341	. . . 4 wff A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
23	22, 17	wex 1480	. . 3 wff E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
24	23, 3	wal 1341	. 2 wff A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
25	24, 7	wal 1341	1 wff A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )

This axiom is referenced by:  sscoll2  13870