Theorem ax6ev 1969

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

Syntax hints:  ¬ wn 3  ∀wal 1538  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  equs4v  2000  alequexv  2001  equsv  2003  equid  2012  ax6evr  2015  aeveq  2057  sbcom2  2174  spimedv  2198  spimfv  2240  equsalv  2268  ax6e  2382  axc15  2421  sb4b  2474  dfeumo  2531  euequ  2591  dfdif3OLD  4089  exel  5401  dmi  5893  1st2val  8005  2nd2val  8006  bnj1468  34844  in-ax8  36209  ss-ax8  36210  bj-ssbeq  36638  bj-ax12  36642  bj-equsexval  36645  bj-ssbid2ALT  36648  bj-ax6elem2  36652  bj-eqs  36660  bj-equsvt  36764  bj-spimtv  36779  bj-dtrucor2v  36802  bj-sbievw1  36830  bj-sbievw  36832  wl-isseteq  37490  wl-equsalvw  37523  wl-equsaldv  37525  wl-sbcom2d  37546  wl-euequf  37559  wl-dfclab  37581  axc11n-16  38923  ax12eq  38926  ax12el  38927  ax12inda  38933  ax12v2-o  38934  sn-exelALT  42198  relexp0eq  43662  ax6e2eq  44519  relopabVD  44862  ax6e2eqVD  44868  ormkglobd  46846  dtrucor3  48720