Theorem ax6ev 1969

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

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1777

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 1778

This theorem is referenced by:  equs4v  1999  alequexv  2000  equsv  2002  equid  2011  ax6evr  2014  aeveq  2056  sbcom2  2169  spimedv  2193  spimfv  2235  equsalv  2262  ax6e  2385  axc15  2424  sb4b  2477  dfeumo  2534  euequ  2594  dfdif3OLD  4135  exel  5456  dmi  5945  1st2val  8054  2nd2val  8055  bnj1468  34814  gg-ax8  36143  bj-ssbeq  36567  bj-ax12  36571  bj-equsexval  36574  bj-ssbid2ALT  36577  bj-ax6elem2  36581  bj-eqs  36589  bj-equsvt  36693  bj-spimtv  36708  bj-dtrucor2v  36731  bj-sbievw1  36759  bj-sbievw  36761  wl-equsalvw  37440  wl-equsaldv  37442  wl-sbcom2d  37463  wl-euequf  37476  wl-dfclab  37498  axc11n-16  38842  ax12eq  38845  ax12el  38846  ax12inda  38852  ax12v2-o  38853  sn-exelALT  42160  relexp0eq  43603  ax6e2eq  44468  relopabVD  44812  ax6e2eqVD  44818  dtrucor3  48450