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

Axiom ax-sn 3189
Description: The singleton axiom. This axiom sets up the existence of a singleton set. This appears to have been an oversight on Hailperin's part, as it is needed to prove the properties of Kuratowski ordered pairs.
Assertion
Ref Expression
ax-sn yz(z yz = x)
Distinct variable group:   x,y,z

Detailed syntax breakdown of Axiom ax-sn
StepHypRef Expression
1 vz . . . . 5 set z
2 vy . . . . 5 set y
31, 2wel 1401 . . . 4 wff z y
4 vx . . . . 5 set x
51, 4weq 1399 . . . 4 wff z = x
63, 5wb 173 . . 3 wff (z yz = x)
76, 1wal 1322 . 2 wff z(z yz = x)
87, 2wex 1327 1 wff yz(z yz = x)
Colors of variables: wff set class
This axiom is referenced by:  snex  3213
  Copyright terms: Public domain W3C validator