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

Theorem a9e 1707
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 1458 through ax-14 2163 and ax-17 1537, all axioms other than ax-9 1542 are believed to be theorems of free logic, although the system without ax-9 1542 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
Assertion
Ref Expression
a9e 𝑥 𝑥 = 𝑦

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1541 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1503
This theorem was proved from axioms:  ax-i9 1541
This theorem is referenced by:  ax9o  1709  equid  1712  equs4  1736  equsal  1738  equsex  1739  equsexd  1740  spimt  1747  spimeh  1750  spimed  1751  equvini  1769  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  euequ1  2133
  Copyright terms: Public domain W3C validator