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

Axiom ax-si 3185
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}}.
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 1397 . . . . . . . 8 class z
32csn 2803 . . . . . . 7 class {z}
4 vw . . . . . . . . 9 set w
54cv 1397 . . . . . . . 8 class w
65csn 2803 . . . . . . 7 class {w}
73, 6copk 2862 . . . . . 6 class ⟪{z}, {w}⟫
8 vy . . . . . . 7 set y
98cv 1397 . . . . . 6 class y
107, 9wcel 1400 . . . . 5 wff ⟪{z}, {w}⟫ y
112, 5copk 2862 . . . . . 6 class z, w
12 vx . . . . . . 7 set x
1312cv 1397 . . . . . 6 class x
1411, 13wcel 1400 . . . . 5 wff z, w x
1510, 14wb 173 . . . 4 wff (⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1615, 4wal 1322 . . 3 wff w(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1716, 1wal 1322 . 2 wff zw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
1817, 8wex 1327 1 wff yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
Colors of variables: wff set class
This axiom is referenced by:  axsiprim  3195  sikexg  3400
  Copyright terms: Public domain W3C validator