NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-si Structured version   GIF version

Axiom ax-si 4083
Description: State the axiom of the singleton image. This axiom guarantees that guarantees the existence of a set that raises the "type" of another set when considered as a relationship. Axiom P2 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
ax-si yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-si
StepHypRef Expression
1 vz . . . . . . . . 9 set z
21cv 1641 . . . . . . . 8 class z
32csn 3737 . . . . . . 7 class {z}
4 vw . . . . . . . . 9 set w
54cv 1641 . . . . . . . 8 class w
65csn 3737 . . . . . . 7 class {w}
73, 6copk 4057 . . . . . 6 class ⟪{z}, {w}⟫
8 vy . . . . . . 7 set y
98cv 1641 . . . . . 6 class y
107, 9wcel 1710 . . . . 5 wff ⟪{z}, {w}⟫ y
112, 5copk 4057 . . . . . 6 class z, w
12 vx . . . . . . 7 set x
1312cv 1641 . . . . . 6 class x
1411, 13wcel 1710 . . . . 5 wff z, w x
1510, 14wb 176 . . . 4 wff (⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1615, 4wal 1540 . . 3 wff w(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1716, 1wal 1540 . 2 wff zw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1817, 8wex 1541 1 wff yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
Colors of variables: wff set class
This axiom is referenced by:  axsiprim  4093  sikexg  4296
  Copyright terms: Public domain W3C validator