Theorem ax6ev 2002

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 2000

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  equs4v  2033  alequexv  2034  equsv  2036  equid  2045  ax6evr  2048  aeveq  2091  sbcom2  2210  spimedv  2236  spimfv  2278  equsalv  2305  ax6e  2417  axc15  2456  sb4b  2509  dfeumo  2566  euequ  2627  exel  5417  dmi  5913  1st2val  8021  2nd2val  8022  elirrv  9567  bnj1468  35304  in-ax8  36798  ss-ax8  36799  bj-ssbeq  37337  bj-ax12  37341  bj-equsexval  37344  bj-ssbid2ALT  37347  bj-ax6elem2  37351  bj-spim0  37353  bj-eqs  37360  bj-equsvt  37458  bj-nnf-spime  37462  bj-spimtv  37491  bj-dtrucor2v  37514  bj-sbievw1  37542  bj-sbievw  37544  wl-isseteq  38213  wl-equsalvw  38255  wl-equsaldv  38257  wl-sbcom2d  38278  wl-euequf  38291  wl-dfclab  38302  axc11n-16  39775  ax12eq  39778  ax12el  39779  ax12inda  39785  ax12v2-o  39786  sn-exelALT  43053  relexp0eq  44505  ax6e2eq  45344  relopabVD  45687  ax6e2eqVD  45693  ormkglobd  47669  dtrucor3  49654