Theorem ax6ev 2001

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567  ∃wex 1811

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

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

This theorem is used by:  equs4v  2032  alequexv  2033  equsv  2035  equid  2044  ax6evr  2047  aeveq  2090  sbcom2  2208  spimedv  2233  spimfv  2275  equsalv  2301  ax6e  2412  axc15  2451  sb4b  2504  dfeumo  2561  euequ  2622  exel  5401  dmi  5902  1st2val  8029  2nd2val  8030  elirrv  9591  bnj1468  35476  in-ax8  37013  ss-ax8  37014  bj-ssbeq  37552  bj-ax12  37556  bj-equsexval  37559  bj-ssbid2ALT  37562  bj-ax6elem2  37566  bj-spim0  37568  bj-eqs  37575  bj-equsvt  37673  bj-nnf-spime  37677  bj-spimtv  37706  bj-dtrucor2v  37729  bj-sbievw1  37757  bj-sbievw  37759  wl-isseteq  38429  wl-equsalvw  38471  wl-equsaldv  38473  wl-sbcom2d  38494  wl-euequf  38507  wl-dfclab  38518  axc11n-16  39996  ax12eq  39999  ax12el  40000  ax12inda  40006  ax12v2-o  40007  sn-exelALT  43274  relexp0eq  44701  ax6e2eq  45540  relopabVD  45883  ax6e2eqVD  45889  ormkglobd  47887  dtrucor3  49909