MPE Home 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 2383. When possible, use of this theorem rather than ax6e 2383 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 230 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 206  df-ex 1783
This theorem is referenced by:  equs4v  2003  alequexv  2004  equsv  2006  equid  2015  ax6evr  2018  aeveq  2059  sbcom2  2161  spimedv  2190  spimfv  2232  equsalv  2259  ax6e  2383  axc15  2422  sb4b  2475  sb4bOLD  2476  dfeumo  2537  euequ  2597  dfdif3  4049  dmi  5830  1st2val  7859  2nd2val  7860  bnj1468  32826  bj-ssbeq  34834  bj-ax12  34838  bj-equsexval  34841  bj-ssbid2ALT  34844  bj-ax6elem2  34848  bj-eqs  34856  bj-equsvt  34961  bj-spimtv  34976  bj-dtrucor2v  35000  bj-sbievw1  35029  bj-sbievw  35031  wl-equsalvw  35697  wl-sbcom2d  35716  wl-euequf  35729  wl-dfclab  35747  axc11n-16  36952  ax12eq  36955  ax12el  36956  ax12inda  36962  ax12v2-o  36963  sn-el  40187  relexp0eq  41309  ax6e2eq  42177  relopabVD  42521  ax6e2eqVD  42527  dtrucor3  46144
  Copyright terms: Public domain W3C validator