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

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

Usage of this theorem is discouraged because it depends on ax-13 2386. It is preferred to use ax6ev 1968 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2388 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 2176 . 2 (𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
2 ax13lem1 2388 . . . 4 𝑥 = 𝑦 → (𝑤 = 𝑦 → ∀𝑥 𝑤 = 𝑦))
3 ax6ev 1968 . . . . . 6 𝑥 𝑥 = 𝑤
4 equtr 2024 . . . . . 6 (𝑥 = 𝑤 → (𝑤 = 𝑦𝑥 = 𝑦))
53, 4eximii 1833 . . . . 5 𝑥(𝑤 = 𝑦𝑥 = 𝑦)
6519.35i 1875 . . . 4 (∀𝑥 𝑤 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
72, 6syl6com 37 . . 3 (𝑤 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦))
8 ax6ev 1968 . . 3 𝑤 𝑤 = 𝑦
97, 8exlimiiv 1928 . 2 𝑥 = 𝑦 → ∃𝑥 𝑥 = 𝑦)
101, 9pm2.61i 184 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1531  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173  ax-13 2386
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777
This theorem is referenced by:  ax6  2398  spimt  2400  spim  2401  spimed  2402  spimvALT  2405  spei  2408  equs4  2434  equsal  2435  equsexALT  2437  equvini  2473  equviniOLD  2474  equvel  2475  2ax6elem  2489  axi9  2787  dtrucor2  5272  axextnd  10012  ax8dfeq  33043  bj-axc10  34105  bj-alequex  34106  ax6er  34156  exlimiieq1  34157  wl-exeq  34773  wl-equsald  34778  ax6e2nd  40890  ax6e2ndVD  41240  ax6e2ndALT  41262  spd  44780
  Copyright terms: Public domain W3C validator