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

Step	Hyp	Ref	Expression
1		ax9v 1655	. 2 ⊢ ¬ ∀x ¬ x = y
2		df-ex 1542	. 2 ⊢ (∃x x = y ↔ ¬ ∀x ¬ x = y)
3	1, 2	mpbir 200	1 ⊢ ∃x x = y

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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