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

Theorem ax6ev 2072
Description: At least one individual exists. Weaker version of ax6e 2356. When possible, use of this theorem rather than ax6e 2356 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 2071 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1875 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 222 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 2070
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  exiftru  2073  spimeh  2095  equs4v  2100  equsalvw  2101  equsexvw  2102  equid  2109  ax6evr  2112  equvinvOLD  2128  aeveq  2149  19.8a  2214  equsalv  2273  equsexv  2274  spimv1  2291  equsalhwOLD  2300  ax6e  2356  axc15  2403  sbcom2  2537  euexOLD  2619  axext3  2745  dfdif3  3884  dmi  5510  snnexOLD  7167  1st2val  7396  2nd2val  7397  bnj1468  31367  bj-sbex  33066  bj-ssbeq  33067  bj-ssb0  33068  bj-ssb1  33073  bj-equsexval  33077  bj-ssbid2ALT  33085  bj-ax6elem2  33091  bj-alequexv  33094  bj-eqs  33102  bj-spimtv  33156  bj-spimedv  33157  bj-spimvv  33159  bj-speiv  33162  bj-dtrucor2v  33234  bj-cleljustab  33279  wl-sbcom2d  33772  wl-euequf  33784  axc11n-16  34897  ax12eq  34900  ax12el  34901  ax12inda  34907  ax12v2-o  34908  relexp0eq  38671  ax6e2eq  39438  relopabVD  39792  ax6e2eqVD  39798
  Copyright terms: Public domain W3C validator