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

Theorem ax6ev 1817
Description: At least one individual exists. Weaker version of ax6e 2104. When possible, use of this theorem rather than ax6e 2104 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 1816 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1674 . 2  |-  ( E. x  x  =  y  <->  -.  A. x  -.  x  =  y )
31, 2mpbir 214 1  |-  E. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1452   E.wex 1673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1815
This theorem depends on definitions:  df-bi 190  df-ex 1674
This theorem is referenced by:  exiftru  1818  spimeh  1851  equs4v  1856  equsalvw  1857  equsexvw  1858  equid  1865  equidOLD  1866  ax6evr  1869  equviniv  1882  ax12v  1944  19.8a  1945  19.8aOLD  1946  aev  2036  equsalhw  2038  spimv1  2068  cbv3hvOLD  2072  cbv3hvOLDOLD  2073  equsexv  2076  ax6e  2104  axc11n  2153  axc11nALT  2154  ax12v2  2185  sbcom2  2284  euequ1  2315  euex  2333  axext3  2443  dmi  5067  snnex  6623  1st2val  6845  2nd2val  6846  bnj1468  29705  bj-sbex  31283  bj-ssbeq  31284  bj-ssb0  31285  bj-ssb1  31290  bj-equsexval  31295  bj-ssbid2ALT  31303  bj-ax6elem2  31309  bj-spimtv  31363  bj-spimedv  31364  bj-spimvv  31366  bj-speiv  31369  bj-equsalv  31389  bj-axc11nv  31392  bj-axc15v  31406  bj-dtrucor2v  31460  wl-sbcom2d  31935  wl-euequ1f  31947  wl-ax12v2  31953  wl-19.8a  31954  wl-ax12v3  31956  axc11n-16  32553  ax12eq  32556  ax12el  32557  ax12inda  32563  ax12v2-o  32564  relexp0eq  36337  ax6e2eq  36967  relopabVD  37337  ax6e2eqVD  37343
  Copyright terms: Public domain W3C validator