NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-sn Unicode 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
Distinct variable group:   ,,

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