ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a9e Unicode version

Theorem a9e 1631
Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1381 through ax-14 1450 and ax-17 1464, all axioms other than ax-9 1469 are believed to be theorems of free logic, although the system without ax-9 1469 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
Assertion
Ref Expression
a9e  |-  E. x  x  =  y

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1468 1  |-  E. x  x  =  y
Colors of variables: wff set class
Syntax hints:   E.wex 1426
This theorem was proved from axioms:  ax-i9 1468
This theorem is referenced by:  ax9o  1633  equid  1634  equs4  1660  equsal  1662  equsex  1663  equsexd  1664  spimt  1671  spimeh  1674  spimed  1675  equvini  1688  ax11v2  1748  ax11v  1755  ax11ev  1756  equs5or  1758  euequ1  2043
  Copyright terms: Public domain W3C validator