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

Theorem ax6ev 1877
Description: At least one individual exists. Weaker version of ax6e 2238. When possible, use of this theorem rather than ax6e 2238 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 1876 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1696 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 220 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1473  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1875
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  exiftru  1878  spimeh  1912  equs4v  1917  equsalvw  1918  equsexvw  1919  equid  1926  ax6evr  1929  equvinv  1946  equvinivOLD  1948  aeveq  1969  ax12vOLDOLD  2038  19.8a  2039  19.8aOLD  2040  equsexv  2095  spimv1  2101  equsalhw  2109  aevOLD  2148  cbv3hvOLD  2161  cbv3hvOLDOLD  2162  ax6e  2238  axc15  2291  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  ax12v2OLD  2330  sbcom2  2433  euex  2482  axext3  2592  dmi  5261  snnex  6862  1st2val  7085  2nd2val  7086  bnj1468  30170  bj-sbex  31815  bj-ssbeq  31816  bj-ssb0  31817  bj-ssb1  31822  bj-equsexval  31827  bj-ssbid2ALT  31835  bj-ax6elem2  31841  bj-eqs  31850  bj-spimtv  31905  bj-spimedv  31906  bj-spimvv  31908  bj-speiv  31911  bj-equsalv  31931  bj-dtrucor2v  31989  wl-sbcom2d  32523  wl-euequ1f  32535  axc11n-16  33241  ax12eq  33244  ax12el  33245  ax12inda  33251  ax12v2-o  33252  relexp0eq  37012  ax6e2eq  37794  relopabVD  38159  ax6e2eqVD  38165
  Copyright terms: Public domain W3C validator