Axiom ax-ins2 4085

Description: State the insertion two axiom. This axiom sets up a set that inserts an extra variable at the second place of the relationship described by x. Axiom P3 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-ins2	|- E.yA.zA.wA.t(<<{{z}}, <<w, t>>>> e. y <-> <<z, t>> e. x)

Distinct variable group:   x,y,z,w,t

Detailed syntax breakdown of Axiom ax-ins2

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

This axiom is referenced by:  axins2prim  4096  ins2kexg  4306