Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  a9e Unicode version

Theorem a9e 1948
 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 1563 through ax-14 1725 and ax-17 1623, all axioms other than ax9 1949 are believed to be theorems of free logic, although the system without ax9 1949 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 25-Feb-2018.)
Assertion
Ref Expression
a9e

Proof of Theorem a9e
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 19.8a 1758 . 2
2 a9ev 1664 . . 3
3 ax12v 1947 . . . . . 6
4 a9ev 1664 . . . . . . . 8
5 equequ2 1694 . . . . . . . . 9
65biimprcd 217 . . . . . . . 8
74, 6eximii 1584 . . . . . . 7
8719.35i 1608 . . . . . 6
93, 8syl6com 33 . . . . 5
109equcoms 1689 . . . 4
1110exlimiv 1641 . . 3
122, 11ax-mp 8 . 2
131, 12pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4  wal 1546  wex 1547 This theorem is referenced by:  ax9  1949  equs4  1951  equs4OLD  1952  spimt  1953  spim  1955  spimed  1958  spei  1964  equsal  1966  equvini  2040  ax11vALT  2144  axi9  2378  dtrucor2  4353  axextnd  8413  ax13dfeq  25193  a9e2nd  28004  a9e2ndVD  28377  a9e2ndALT  28400 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-12 1946 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
 Copyright terms: Public domain W3C validator