Theorem ax6ev 1996

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

Syntax hints:  ¬ wn 3  ∀wal 1565  ∃wex 1806

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

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

This theorem is referenced by:  equs4v  2027  alequexv  2028  equsv  2030  equid  2039  ax6evr  2042  aeveq  2085  sbcom2  2213  spimedv  2239  spimfv  2281  equsalv  2309  ax6e  2421  axc15  2460  sb4b  2513  dfeumo  2570  euequ  2631  dfdif3OLD  4081  exel  5416  dmi  5912  1st2val  8014  2nd2val  8015  elirrv  9559  bnj1468  35179  in-ax8  36659  ss-ax8  36660  bj-ssbeq  37198  bj-ax12  37202  bj-equsexval  37205  bj-ssbid2ALT  37208  bj-ax6elem2  37212  bj-spim0  37214  bj-eqs  37221  bj-equsvt  37319  bj-nnf-spime  37323  bj-spimtv  37352  bj-dtrucor2v  37375  bj-sbievw1  37403  bj-sbievw  37405  wl-isseteq  38073  wl-equsalvw  38115  wl-equsaldv  38117  wl-sbcom2d  38138  wl-euequf  38151  wl-dfclab  38162  axc11n-16  39636  ax12eq  39639  ax12el  39640  ax12inda  39646  ax12v2-o  39647  sn-exelALT  42914  relexp0eq  44353  ax6e2eq  45192  relopabVD  45535  ax6e2eqVD  45541  ormkglobd  47517  dtrucor3  49496