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

Theorem ax6ev 1712
Description: At least one individual exists. Weaker version of ax6e 1955. When possible, use of this theorem rather than ax6e 1955 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)
Assertion
Ref Expression
ax6ev  |-  E. x  x  =  y
Distinct variable group:    x, y

Proof of Theorem ax6ev
StepHypRef Expression
1 ax6v 1711 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1588 . 2  |-  ( E. x  x  =  y  <->  -.  A. x  -.  x  =  y )
31, 2mpbir 209 1  |-  E. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1368   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1710
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  exiftru  1713  spimeh  1722  equid  1731  equviniv  1743  19.8a  1795  aev  1878  equsalhw  1880  cbv3hv  1891  ax6e  1955  axc11n  2006  axc11nOLD  2007  ax12v2  2040  ax12vALT  2138  sbcom2  2158  axc11n-16  2246  ax12eq  2249  ax12el  2250  ax12inda  2256  ax12v2-o  2257  euequ1  2266  euex  2288  euequ1OLD  2382  relop  5088  dmi  5152  snnex  6482  1st2val  6702  2nd2val  6703  wl-sbcom2d  28525  ax6e2eq  31566  relopabVD  31937  ax6e2eqVD  31943  bnj1468  32139  bnj1014  32253  bj-spimtv  32514  bj-spimv  32515  bj-spimedv  32516  bj-speiv  32521  bj-equs4v  32545  bj-equsalv  32546  bj-axc11nv  32551  bj-axc15v  32565  bj-dtrucor2v  32622
  Copyright terms: Public domain W3C validator