Theorem ax6ev 1947

Description: At least one individual exists. Weaker version of ax6e 2286. When possible, use of this theorem rather than ax6e 2286 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)

Assertion

Ref	Expression
ax6ev	⊢ ∃𝑥 𝑥 = 𝑦

Distinct variable group:   𝑥,𝑦

Proof of Theorem ax6ev

Step	Hyp	Ref	Expression
1		ax6v 1946	. 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2		df-ex 1745	. 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
3	1, 2	mpbir 221	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1521  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1945

This theorem depends on definitions:  df-bi 197  df-ex 1745

This theorem is referenced by:  exiftru  1948  spimeh  1971  equs4v  1976  equsalvw  1977  equsexvw  1978  equid  1985  ax6evr  1988  equvinv  2003  aeveq  2024  19.8a  2090  equsalv  2146  equsexv  2147  spimv1  2153  equsalhw  2161  ax6e  2286  axc15  2339  axc11nOLD  2343  sbcom2  2473  euex  2522  axext3  2633  dmi  5372  snnexOLD  7009  1st2val  7238  2nd2val  7239  bnj1468  31042  bj-sbex  32751  bj-ssbeq  32752  bj-ssb0  32753  bj-ssb1  32758  bj-equsexval  32763  bj-ssbid2ALT  32771  bj-ax6elem2  32777  bj-alequexv  32780  bj-eqs  32788  bj-spimtv  32843  bj-spimedv  32844  bj-spimvv  32846  bj-speiv  32849  bj-dtrucor2v  32926  bj-cleljustab  32972  wl-sbcom2d  33474  wl-euequ1f  33486  axc11n-16  34542  ax12eq  34545  ax12el  34546  ax12inda  34552  ax12v2-o  34553  relexp0eq  38310  ax6e2eq  39090  relopabVD  39451  ax6e2eqVD  39457