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

Theorem ax6ev 1973
 Description: At least one individual exists. Weaker version of ax6e 2391. When possible, use of this theorem rather than ax6e 2391 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)
Assertion
Ref Expression
ax6ev 𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem ax6ev
StepHypRef Expression
1 ax6v 1972 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1783 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 234 1 𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1782 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1971 This theorem depends on definitions:  df-bi 210  df-ex 1783 This theorem is referenced by:  spimehOLD  1976  exgenOLD  1980  equs4v  2007  alequexv  2008  equsv  2010  equsexvwOLD  2013  equid  2020  ax6evr  2023  aeveq  2062  sbcom2  2166  spimedv  2196  spimfv  2240  equsalv  2266  equsexv  2267  ax6e  2391  axc15  2434  sb4b  2489  sb4bOLD  2490  dfeumo  2555  euequ  2618  dfdif3  4021  dmi  5760  1st2val  7719  2nd2val  7720  bnj1468  32336  bj-ssbeq  34370  bj-ax12  34374  bj-equsexval  34377  bj-ssbid2ALT  34380  bj-ax6elem2  34384  bj-eqs  34392  bj-spimtv  34502  bj-dtrucor2v  34526  bj-sbievw1  34555  bj-sbievw  34557  wl-equsalvw  35213  wl-sbcom2d  35232  wl-euequf  35245  wl-dfclab  35263  axc11n-16  36504  ax12eq  36507  ax12el  36508  ax12inda  36514  ax12v2-o  36515  sn-el  39691  relexp0eq  40765  ax6e2eq  41626  relopabVD  41970  ax6e2eqVD  41976
 Copyright terms: Public domain W3C validator