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

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

It is preferred to use ax6ev 1877 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2236 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 2039 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2236 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1877 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 1935 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1754 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1795 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 36 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1877 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1846 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 175 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1473  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696
This theorem is referenced by:  ax6  2239  spimt  2241  spim  2242  spimed  2243  spimv  2245  spei  2249  equs4  2278  equsal  2279  equsexALT  2282  equvini  2334  equvel  2335  2ax6elem  2437  axi9  2586  dtrucor2  4828  axextnd  9292  ax8dfeq  30948  bj-axc10  31894  bj-alequex  31895  ax6er  32008  exlimiieq1  32009  wl-exeq  32500  wl-equsald  32504  ax6e2nd  37795  ax6e2ndVD  38166  ax6e2ndALT  38188  spd  42223
  Copyright terms: Public domain W3C validator