Theorem ax6ev 1972

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

Syntax hints:  ¬ wn 3  ∀wal 1536  ∃wex 1781

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

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

This theorem is referenced by:  spimehOLD  1975  exgenOLD  1979  equs4v  2006  alequexv  2007  equsv  2009  equsexvwOLD  2012  equid  2019  ax6evr  2022  aeveq  2061  sbcom2  2165  spimedv  2195  spimfv  2239  equsalv  2265  equsexv  2266  ax6e  2390  axc15  2433  sb4b  2488  sb4bOLD  2489  dfeumo  2595  euequ  2658  dfdif3  4042  dmi  5755  1st2val  7699  2nd2val  7700  bnj1468  32228  bj-ssbeq  34099  bj-ax12  34103  bj-equsexval  34106  bj-ssbid2ALT  34109  bj-ax6elem2  34113  bj-eqs  34121  bj-spimtv  34231  bj-dtrucor2v  34255  bj-sbievw1  34284  bj-sbievw  34286  wl-equsalvw  34943  wl-sbcom2d  34962  wl-euequf  34975  wl-dfclab  34993  axc11n-16  36234  ax12eq  36237  ax12el  36238  ax12inda  36244  ax12v2-o  36245  sn-el  39402  relexp0eq  40402  ax6e2eq  41263  relopabVD  41607  ax6e2eqVD  41613