Axiom ax-sscoll 13174

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	|- A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( 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 1330	. . . . . . . 8 class b
5	1, 2, 4	wrex 2415	. . . . . . 7 wff E. y e. b ph
6		vx	. . . . . . 7 setvar x
7		va	. . . . . . . 8 setvar a
8	7	cv 1330	. . . . . . 7 class a
9	5, 6, 8	wral 2414	. . . . . 6 wff A. x e. a E. y e. b ph
10		vd	. . . . . . . . . 10 setvar d
11	2, 10	wel 1481	. . . . . . . . 9 wff y e. d
12	1, 6, 8	wrex 2415	. . . . . . . . 9 wff E. x e. a ph
13	11, 12	wb 104	. . . . . . . 8 wff ( y e. d <-> E. x e. a ph )
14	13, 2	wal 1329	. . . . . . 7 wff A. y ( y e. d <-> E. x e. a ph )
15		vc	. . . . . . . 8 setvar c
16	15	cv 1330	. . . . . . 7 class c
17	14, 10, 16	wrex 2415	. . . . . 6 wff E. d e. c A. y ( y e. d <-> E. x e. a ph )
18	9, 17	wi 4	. . . . 5 wff ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )
19		vz	. . . . 5 setvar z
20	18, 19	wal 1329	. . . 4 wff A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )
21	20, 15	wex 1468	. . 3 wff E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )
22	21, 3	wal 1329	. 2 wff A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )
23	22, 7	wal 1329	1 wff A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )

This axiom is referenced by:  sscoll2  13175