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

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

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1469 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1427
This theorem was proved from axioms:  ax-i9 1469
This theorem is referenced by:  ax9o  1634  equid  1635  equs4  1661  equsal  1663  equsex  1664  equsexd  1665  spimt  1672  spimeh  1675  spimed  1676  equvini  1689  ax11v2  1749  ax11v  1756  ax11ev  1757  equs5or  1759  euequ1  2044
  Copyright terms: Public domain W3C validator