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

Theorem a9ev 1646
Description: At least one individual exists. Weaker version of a9e 1904. When possible, use of this theorem rather than a9e 1904 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 1645 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1532 . 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 1530   E.wex 1531
This theorem is referenced by:  exiftru  1647  a16g  1898  ax11v2  1945  pm11.07  2067  ax10-16  2142  ax11eq  2145  ax11el  2146  ax11inda  2152  ax11v2-o  2153  euequ1  2244  snnex  4540  relop  4850  dmi  4909  1st2val  6161  2nd2val  6162  a9e2eq  28622  relopabVD  28993  a9e2eqVD  28999  bnj1468  29194  bnj1014  29308  ax11v2NEW7  29505  a16gNEW7  29521  pm11.07OLD7  29716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-9 1644
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator