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

Theorem ax6ev 1754
Description: At least one individual exists. Weaker version of ax6e 2007. When possible, use of this theorem rather than ax6e 2007 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 1753 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1618 . 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 1396   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1752
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  exiftru  1755  spimeh  1787  equs4v  1792  equid  1796  equviniv  1808  ax12v  1860  ax12vOLD  1861  19.8a  1862  19.8aOLD  1863  aev  1948  equsalhw  1950  cbv3hv  1961  ax6e  2007  axc11n  2053  axc11nOLD  2054  ax12v2  2087  sbcom2  2191  axc11n-16  2270  ax12eq  2273  ax12el  2274  ax12inda  2280  ax12v2-o  2281  euequ1  2290  euex  2310  euequ1OLD  2384  axext3  2434  relop  5142  dmi  5206  snnex  6579  1st2val  6799  2nd2val  6800  wl-sbcom2d  30254  ax6e2eq  33743  relopabVD  34121  ax6e2eqVD  34127  bnj1468  34324  bj-spimtv  34698  bj-spimv  34699  bj-spimedv  34700  bj-speiv  34705  bj-equsalv  34729  bj-equsalvv  34730  bj-axc11nv  34736  bj-axc15v  34750  bj-dtrucor2v  34807  relexp0eq  38239
  Copyright terms: Public domain W3C validator