 New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  a9ev GIF version

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

Proof of Theorem a9ev
StepHypRef Expression
1 ax9v 1655 . 2 ¬ x ¬ x = y
2 df-ex 1542 . 2 (x x = y ↔ ¬ x ¬ x = y)
31, 2mpbir 200 1 x x = y
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1541 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-9 1654 This theorem depends on definitions:  df-bi 177  df-ex 1542 This theorem is referenced by:  exiftru  1657  exiftruOLD  1658  spimeh  1667  equid  1676  sp  1747  equsalhw  1838  cbv3hv  1850  a16g  1945  ax11v2  1992  pm11.07  2115  ax10-16  2190  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  euequ1  2292
 Copyright terms: Public domain W3C validator