Axiom ax-typlower 4087

Description: The type lowering axiom. This axiom eventually sets up both the existence of the sum set and the existence of the range of a relationship. Axiom P6 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-typlower	|- E.yA.z(z e. y <-> A.w<<w, {z}>> e. x)

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-typlower

Step	Hyp	Ref	Expression
1		vz	. . . . 5 setvar z
2		vy	. . . . 5 setvar y
3	1, 2	wel 1711	. . . 4 wff z e. y
4		vw	. . . . . . . 8 setvar w
5	4	cv 1641	. . . . . . 7 class w
6	1	cv 1641	. . . . . . . 8 class z
7	6	csn 3738	. . . . . . 7 class {z}
8	5, 7	copk 4058	. . . . . 6 class <<w, {z}>>
9		vx	. . . . . . 7 setvar x
10	9	cv 1641	. . . . . 6 class x
11	8, 10	wcel 1710	. . . . 5 wff <<w, {z}>> e. x
12	11, 4	wal 1540	. . . 4 wff A.w<<w, {z}>> e. x
13	3, 12	wb 176	. . 3 wff (z e. y <-> A.w<<w, {z}>> e. x)
14	13, 1	wal 1540	. 2 wff A.z(z e. y <-> A.w<<w, {z}>> e. x)
15	14, 2	wex 1541	1 wff E.yA.z(z e. y <-> A.w<<w, {z}>> e. x)

This axiom is referenced by:  axtyplowerprim  4095  p6exg  4291