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

Theorem a9e 1696
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 1447 through ax-14 2151 and ax-17 1526, all axioms other than ax-9 1531 are believed to be theorems of free logic, although the system without ax-9 1531 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 1530 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1492
This theorem was proved from axioms:  ax-i9 1530
This theorem is referenced by:  ax9o  1698  equid  1701  equs4  1725  equsal  1727  equsex  1728  equsexd  1729  spimt  1736  spimeh  1739  spimed  1740  equvini  1758  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  euequ1  2121
  Copyright terms: Public domain W3C validator