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	⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ 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⟫⟫ ∈ 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⟫ ∈ x
18	13, 17	wb 176	. . . . 5 wff (⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
19	18, 7	wal 1540	. . . 4 wff ∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
20	19, 5	wal 1540	. . 3 wff ∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
21	20, 1	wal 1540	. 2 wff ∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
22	21, 11	wex 1541	1 wff ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)

This axiom is referenced by:  axins2prim  4096  ins2kexg  4306