Theorem ax6ev 1969

Description: At least one individual exists. Weaker version of ax6e 2381. When possible, use of this theorem rather than ax6e 2381 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  2381  axc15  2420  sb4b  2473  dfeumo  2530  euequ  2590  dfdif3OLD  4077  exel  5388  dmi  5875  1st2val  7975  2nd2val  7976  bnj1468  34829  in-ax8  36205  ss-ax8  36206  bj-ssbeq  36634  bj-ax12  36638  bj-equsexval  36641  bj-ssbid2ALT  36644  bj-ax6elem2  36648  bj-eqs  36656  bj-equsvt  36760  bj-spimtv  36775  bj-dtrucor2v  36798  bj-sbievw1  36826  bj-sbievw  36828  wl-isseteq  37486  wl-equsalvw  37519  wl-equsaldv  37521  wl-sbcom2d  37542  wl-euequf  37555  wl-dfclab  37577  axc11n-16  38924  ax12eq  38927  ax12el  38928  ax12inda  38934  ax12v2-o  38935  sn-exelALT  42199  relexp0eq  43683  ax6e2eq  44540  relopabVD  44883  ax6e2eqVD  44889  ormkglobd  46866  dtrucor3  48780