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  4083  exel  5395  dmi  5887  1st2val  7998  2nd2val  7999  bnj1468  34842  in-ax8  36207  ss-ax8  36208  bj-ssbeq  36636  bj-ax12  36640  bj-equsexval  36643  bj-ssbid2ALT  36646  bj-ax6elem2  36650  bj-eqs  36658  bj-equsvt  36762  bj-spimtv  36777  bj-dtrucor2v  36800  bj-sbievw1  36828  bj-sbievw  36830  wl-isseteq  37488  wl-equsalvw  37521  wl-equsaldv  37523  wl-sbcom2d  37544  wl-euequf  37557  wl-dfclab  37579  axc11n-16  38926  ax12eq  38929  ax12el  38930  ax12inda  38936  ax12v2-o  38937  sn-exelALT  42201  relexp0eq  43683  ax6e2eq  44540  relopabVD  44883  ax6e2eqVD  44889  ormkglobd  46866  dtrucor3  48777