MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax6e Structured version   Visualization version   GIF version

Theorem ax6e 2249
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-4 1734 through ax-9 1996, all axioms other than ax-6 1885 are believed to be theorems of free logic, although the system without ax-6 1885 is not complete in free logic.

It is preferred to use ax6ev 1887 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2247 became available. (Revised by Wolf Lammen, 8-Sep-2018.)

Assertion
Ref Expression
ax6e 𝑥 𝑥 = 𝑦

Proof of Theorem ax6e
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 19.8a 2049 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2247 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1887 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 1945 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1761 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1803 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1887 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1856 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 176 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  ax6  2250  spimt  2252  spim  2253  spimed  2254  spimv  2256  spei  2260  equs4  2289  equsal  2290  equsexALT  2293  equvini  2345  equvel  2346  2ax6elem  2448  axi9  2597  dtrucor2  4862  axextnd  9357  ax8dfeq  31402  bj-axc10  32346  bj-alequex  32347  ax6er  32460  exlimiieq1  32461  wl-exeq  32950  wl-equsald  32954  ax6e2nd  38253  ax6e2ndVD  38624  ax6e2ndALT  38646  spd  41714
  Copyright terms: Public domain W3C validator