Theorem ax6ev 1973

Description: At least one individual exists. Weaker version of ax6e 2391. When possible, use of this theorem rather than ax6e 2391 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 1972	. 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2		df-ex 1783	. 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
3	1, 2	mpbir 234	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1782

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

This theorem depends on definitions:  df-bi 210  df-ex 1783

This theorem is referenced by:  spimehOLD  1976  exgenOLD  1980  equs4v  2007  alequexv  2008  equsv  2010  equsexvwOLD  2013  equid  2020  ax6evr  2023  aeveq  2062  sbcom2  2166  spimedv  2196  spimfv  2240  equsalv  2266  equsexv  2267  ax6e  2391  axc15  2434  sb4b  2489  sb4bOLD  2490  dfeumo  2555  euequ  2618  dfdif3  4021  dmi  5760  1st2val  7719  2nd2val  7720  bnj1468  32336  bj-ssbeq  34370  bj-ax12  34374  bj-equsexval  34377  bj-ssbid2ALT  34380  bj-ax6elem2  34384  bj-eqs  34392  bj-spimtv  34502  bj-dtrucor2v  34526  bj-sbievw1  34555  bj-sbievw  34557  wl-equsalvw  35213  wl-sbcom2d  35232  wl-euequf  35245  wl-dfclab  35263  axc11n-16  36504  ax12eq  36507  ax12el  36508  ax12inda  36514  ax12v2-o  36515  sn-el  39691  relexp0eq  40765  ax6e2eq  41626  relopabVD  41970  ax6e2eqVD  41976