Axiom ax-sset 4083

Description: State the axiom of the subset relationship. This axiom guarantees the existence of the Kuratowski relationship representing subset. Slight generalization of axiom P9 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-sset	⊢ ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-sset

Step	Hyp	Ref	Expression
1		vy	. . . . . . . 8 setvar y
2	1	cv 1641	. . . . . . 7 class y
3		vz	. . . . . . . 8 setvar z
4	3	cv 1641	. . . . . . 7 class z
5	2, 4	copk 4058	. . . . . 6 class ⟪y, z⟫
6		vx	. . . . . . 7 setvar x
7	6	cv 1641	. . . . . 6 class x
8	5, 7	wcel 1710	. . . . 5 wff ⟪y, z⟫ ∈ x
9		vw	. . . . . . . 8 setvar w
10	9, 1	wel 1711	. . . . . . 7 wff w ∈ y
11	9, 3	wel 1711	. . . . . . 7 wff w ∈ z
12	10, 11	wi 4	. . . . . 6 wff (w ∈ y → w ∈ z)
13	12, 9	wal 1540	. . . . 5 wff ∀w(w ∈ y → w ∈ z)
14	8, 13	wb 176	. . . 4 wff (⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
15	14, 3	wal 1540	. . 3 wff ∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
16	15, 1	wal 1540	. 2 wff ∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))
17	16, 6	wex 1541	1 wff ∃x∀y∀z(⟪y, z⟫ ∈ x ↔ ∀w(w ∈ y → w ∈ z))

This axiom is used by:  axssetprim  4093  ssetkex  4295