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

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

It is preferred to use ax6ev 2044 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2381 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 2187 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2381 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 2044 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2091 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1901 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1943 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 2044 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1996 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 176 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1618  wex 1841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-12 2184  ax-13 2379
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842
This theorem is referenced by:  ax6  2384  spimt  2386  spim  2387  spimed  2388  spimv  2390  spei  2394  equs4  2423  equsal  2424  equsexALT  2426  equvini  2471  equvel  2472  2ax6elem  2574  axi9  2724  dtrucor2  5038  axextnd  9576  ax8dfeq  31980  bj-axc10  32984  bj-alequex  32985  ax6er  33097  exlimiieq1  33098  wl-exeq  33603  wl-equsald  33607  ax6e2nd  39245  ax6e2ndVD  39612  ax6e2ndALT  39634  spd  42904
  Copyright terms: Public domain W3C validator