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

Axiom ax-sn 4087
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. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
ax-sn
Distinct variable group:   ,,

Detailed syntax breakdown of Axiom ax-sn
StepHypRef Expression
1 vz . . . . 5
2 vy . . . . 5
31, 2wel 1711 . . . 4
4 vx . . . . 5
51, 4weq 1643 . . . 4
63, 5wb 176 . . 3
76, 1wal 1540 . 2
87, 2wex 1541 1
Colors of variables: wff setvar class
This axiom is referenced by:  snex  4111
  Copyright terms: Public domain W3C validator