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

Theorem a9ev 1668
Description: At least one individual exists. Weaker version of a9e 1952. When possible, use of this theorem rather than a9e 1952 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 1667 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1551 . 2  |-  ( E. x  x  =  y  <->  -.  A. x  -.  x  =  y )
31, 2mpbir 201 1  |-  E. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1549   E.wex 1550
This theorem is referenced by:  exiftru  1669  exiftruOLD  1670  spimeh  1679  equid  1688  19.8a  1762  equsalhw  1860  cbv3hv  1878  a9e  1952  ax10  2025  a16gOLD  2049  ax11v2  2078  ax11v2OLD  2079  pm11.07OLD  2192  ax10-16  2267  ax11eq  2270  ax11el  2271  ax11inda  2277  ax11v2-o  2278  euequ1  2369  snnex  4713  relop  5023  dmi  5084  1st2val  6372  2nd2val  6373  a9e2eq  28644  relopabVD  29013  a9e2eqVD  29019  bnj1468  29217  bnj1014  29331  ax11v2NEW7  29530  a16gNEW7  29546
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-9 1666
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator