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	⊢ ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ 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 ∈ 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}⟫ ∈ x
12	11, 4	wal 1540	. . . 4 wff ∀w⟪w, {z}⟫ ∈ x
13	3, 12	wb 176	. . 3 wff (z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)
14	13, 1	wal 1540	. 2 wff ∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)
15	14, 2	wex 1541	1 wff ∃y∀z(z ∈ y ↔ ∀w⟪w, {z}⟫ ∈ x)

This axiom is referenced by:  axtyplowerprim  4095  p6exg  4291