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	|- A. a ( A. x e. a E. y ph -> E. b A. y ( 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 1421	. . . 4 wff E. y ph
4		vx	. . . 4 setvar x
5		va	. . . . 5 setvar a
6	5	cv 1283	. . . 4 class a
7	3, 4, 6	wral 2348	. . 3 wff A. x e. a E. y ph
8		vb	. . . . . . 7 setvar b
9	2, 8	wel 1434	. . . . . 6 wff y e. b
10	1, 4, 6	wrex 2349	. . . . . 6 wff E. x e. a ph
11	9, 10	wb 103	. . . . 5 wff ( y e. b <-> E. x e. a ph )
12	11, 2	wal 1282	. . . 4 wff A. y ( y e. b <-> E. x e. a ph )
13	12, 8	wex 1421	. . 3 wff E. b A. y ( y e. b <-> E. x e. a ph )
14	7, 13	wi 4	. 2 wff ( A. x e. a E. y ph -> E. b A. y ( y e. b <-> E. x e. a ph ) )
15	14, 5	wal 1282	1 wff A. a ( A. x e. a E. y ph -> E. b A. y ( y e. b <-> E. x e. a ph ) )

This axiom is referenced by:  strcoll2  10778