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	|- E.xA.yA.z(<<y, z>> e. x <-> A.w(w e. y -> w e. 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>> e. x
9		vw	. . . . . . . 8 setvar w
10	9, 1	wel 1711	. . . . . . 7 wff w e. y
11	9, 3	wel 1711	. . . . . . 7 wff w e. z
12	10, 11	wi 4	. . . . . 6 wff (w e. y -> w e. z)
13	12, 9	wal 1540	. . . . 5 wff A.w(w e. y -> w e. z)
14	8, 13	wb 176	. . . 4 wff (<<y, z>> e. x <-> A.w(w e. y -> w e. z))
15	14, 3	wal 1540	. . 3 wff A.z(<<y, z>> e. x <-> A.w(w e. y -> w e. z))
16	15, 1	wal 1540	. 2 wff A.yA.z(<<y, z>> e. x <-> A.w(w e. y -> w e. z))
17	16, 6	wex 1541	1 wff E.xA.yA.z(<<y, z>> e. x <-> A.w(w e. y -> w e. z))

This axiom is referenced by:  axssetprim  4093  ssetkex  4295