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

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

It is preferred to use ax6ev 1963 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2383 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 2170 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2383 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1963 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2019 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1828 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1870 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1963 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1923 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 183 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167  ax-13 2381
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  ax6  2393  spimt  2395  spim  2396  spimed  2397  spimvALT  2400  spei  2403  equs4  2429  equsal  2430  equsexALT  2432  equvini  2469  equviniOLD  2470  equvel  2471  2ax6elem  2485  axi9  2784  dtrucor2  5264  axextnd  10001  ax8dfeq  32940  bj-axc10  34002  bj-alequex  34003  ax6er  34053  exlimiieq1  34054  wl-exeq  34655  wl-equsald  34660  ax6e2nd  40769  ax6e2ndVD  41119  ax6e2ndALT  41141  spd  44709
  Copyright terms: Public domain W3C validator