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  4069  exel  5377  dmi  5864  1st2val  7952  2nd2val  7953  bnj1468  34819  in-ax8  36208  ss-ax8  36209  bj-ssbeq  36637  bj-ax12  36641  bj-equsexval  36644  bj-ssbid2ALT  36647  bj-ax6elem2  36651  bj-eqs  36659  bj-equsvt  36763  bj-spimtv  36778  bj-dtrucor2v  36801  bj-sbievw1  36829  bj-sbievw  36831  wl-isseteq  37489  wl-equsalvw  37522  wl-equsaldv  37524  wl-sbcom2d  37545  wl-euequf  37558  wl-dfclab  37580  axc11n-16  38927  ax12eq  38930  ax12el  38931  ax12inda  38937  ax12v2-o  38938  sn-exelALT  42201  relexp0eq  43684  ax6e2eq  44541  relopabVD  44884  ax6e2eqVD  44890  ormkglobd  46866  dtrucor3  48793