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

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

Proof of Theorem a9ev
StepHypRef Expression
1 ax9v 1636 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1529 . 2  |-  ( E. x  x  =  y  <->  -.  A. x  -.  x  =  y )
31, 2mpbir 200 1  |-  E. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527   E.wex 1528
This theorem is referenced by:  a16g  1885  ax11v2  1932  pm11.07  2054  ax10-16  2129  ax11eq  2132  ax11el  2133  ax11inda  2139  ax11v2-o  2140  euequ1  2231  snnex  4524  relop  4834  dmi  4893  1st2val  6145  2nd2val  6146  a9e2eq  28323  relopabVD  28677  a9e2eqVD  28683  bnj1468  28878  bnj1014  28992
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-9 1635
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator