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

Theorem a9ev 1664
Description: At least one individual exists. Weaker version of a9e 1948. When possible, use of this theorem rather than a9e 1948 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 1663 . 2  |-  -.  A. x  -.  x  =  y
2 df-ex 1548 . 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 1546   E.wex 1547
This theorem is referenced by:  exiftru  1665  exiftruOLD  1666  spimeh  1675  equid  1684  19.8a  1758  equsalhw  1856  cbv3hv  1874  a9e  1948  ax10  1991  a16gOLD  2013  ax11v2  2045  pm11.07OLD  2165  ax10-16  2240  ax11eq  2243  ax11el  2244  ax11inda  2250  ax11v2-o  2251  euequ1  2342  snnex  4672  relop  4982  dmi  5043  1st2val  6331  2nd2val  6332  a9e2eq  28355  relopabVD  28722  a9e2eqVD  28728  bnj1468  28923  bnj1014  29037  ax11v2NEW7  29234  a16gNEW7  29250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-9 1662
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator