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

Theorem ax6ev 1963
Description: At least one individual exists. Weaker version of ax6e 2394. When possible, use of this theorem rather than ax6e 2394 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 1962 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1772 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 232 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1961
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  spimehOLD  1966  exgenOLD  1970  equs4v  1997  alequexv  1998  equsv  2000  equsexvwOLD  2003  equid  2010  ax6evr  2013  aeveq  2052  spsbeOLD  2080  sbcom2  2158  spimedv  2188  spimfv  2232  equsalv  2259  equsexv  2260  ax6e  2394  axc15  2438  axc15OLD  2439  sb4b  2495  sb4bOLD  2496  equsb1vOLDOLD  2513  sbtvOLD  2515  dfeumo  2615  euequ  2679  dfdif3  4090  dmi  5785  1st2val  7708  2nd2val  7709  bnj1468  32018  bj-ssbeq  33884  bj-ax12  33888  bj-equsexval  33891  bj-ssbid2ALT  33894  bj-ax6elem2  33898  bj-eqs  33906  bj-spimtv  34014  bj-dtrucor2v  34038  bj-sbievw1  34067  bj-sbievw  34069  wl-equsalvw  34660  wl-sbcom2d  34679  wl-euequf  34692  wl-dfclab  34710  axc11n-16  35956  ax12eq  35959  ax12el  35960  ax12inda  35966  ax12v2-o  35967  sn-el  38990  relexp0eq  39926  ax6e2eq  40771  relopabVD  41115  ax6e2eqVD  41121
  Copyright terms: Public domain W3C validator