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

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

It is preferred to use ax6ev 2059 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2410 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 2206 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2410 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 2059 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2106 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1912 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1958 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 2059 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 2011 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 176 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853
This theorem is referenced by:  ax6  2413  spimt  2415  spim  2416  spimed  2417  spimvALT  2420  spei  2423  equs4  2445  equsal  2446  equsexALT  2448  equvini  2492  equvel  2493  2ax6elem  2597  axi9  2747  dtrucor2  5029  axextnd  9613  ax8dfeq  32033  bj-axc10  33037  bj-alequex  33038  ax6er  33148  exlimiieq1  33149  wl-exeq  33649  wl-equsald  33653  ax6e2nd  39292  ax6e2ndVD  39659  ax6e2ndALT  39681  spd  42946
  Copyright terms: Public domain W3C validator