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

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

Usage of this theorem is discouraged because it depends on ax-13 2377. It is preferred to use ax6ev 1969 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2379 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)

Assertion
Ref Expression
ax6e 𝑥 𝑥 = 𝑦

Proof of Theorem ax6e
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 19.8a 2181 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2379 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1969 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2020 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1837 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1878 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1969 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1931 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 182 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177  ax-13 2377
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  ax6  2389  spimt  2391  spim  2392  spimed  2393  spimvALT  2396  spei  2399  equs4  2421  equsal  2422  equsexALT  2424  equvini  2460  equvel  2461  2ax6elem  2475  axi9  2704  dtrucor2  5372  axextnd  10631  ax8dfeq  35799  bj-axc10  36784  bj-alequex  36785  ax6er  36834  exlimiieq1  36835  wl-exeq  37535  wl-equsald  37540  ax6e2nd  44578  ax6e2ndVD  44928  ax6e2ndALT  44950  spd  49197
  Copyright terms: Public domain W3C validator