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

Theorem ax6ev 1965
Description: At least one individual exists. Weaker version of ax6e 2396. When possible, use of this theorem rather than ax6e 2396 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 1964 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1774 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 232 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1528  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1963
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  spimehOLD  1968  exgenOLD  1972  equs4v  1999  alequexv  2000  equsv  2002  equsexvwOLD  2005  equid  2012  ax6evr  2015  aeveq  2054  spsbeOLD  2082  sbcom2  2160  spimedv  2190  spimfv  2234  equsalv  2261  equsexv  2262  ax6e  2396  axc15  2440  axc15OLD  2441  sb4b  2497  sb4bOLD  2498  equsb1vOLDOLD  2515  sbtvOLD  2517  dfeumo  2616  euequ  2680  dfdif3  4094  dmi  5789  1st2val  7711  2nd2val  7712  bnj1468  32006  bj-ssbeq  33872  bj-ax12  33876  bj-equsexval  33879  bj-ssbid2ALT  33882  bj-ax6elem2  33886  bj-eqs  33894  bj-spimtv  34002  bj-dtrucor2v  34026  bj-sbievw1  34055  bj-sbievw  34057  wl-equsalvw  34648  wl-sbcom2d  34666  wl-euequf  34679  wl-dfclab  34697  axc11n-16  35943  ax12eq  35946  ax12el  35947  ax12inda  35953  ax12v2-o  35954  sn-el  38977  relexp0eq  39913  ax6e2eq  40758  relopabVD  41102  ax6e2eqVD  41108
  Copyright terms: Public domain W3C validator