Theorem ax6ev 1971

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

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1781

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

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

This theorem is referenced by:  equs4v  2002  alequexv  2003  equsv  2005  equid  2014  ax6evr  2017  aeveq  2060  sbcom2  2179  spimedv  2205  spimfv  2247  equsalv  2275  ax6e  2387  axc15  2426  sb4b  2479  dfeumo  2536  euequ  2597  dfdif3OLD  4058  exel  5386  dmi  5876  1st2val  7970  2nd2val  7971  bnj1468  34988  in-ax8  36406  ss-ax8  36407  bj-ssbeq  36947  bj-ax12  36951  bj-equsexval  36954  bj-ssbid2ALT  36957  bj-ax6elem2  36961  bj-spim0  36963  bj-eqs  36970  bj-equsvt  37068  bj-nnf-spime  37072  bj-spimtv  37101  bj-dtrucor2v  37124  bj-sbievw1  37152  bj-sbievw  37154  wl-isseteq  37821  wl-equsalvw  37863  wl-equsaldv  37865  wl-sbcom2d  37886  wl-euequf  37899  wl-dfclab  37910  axc11n-16  39384  ax12eq  39387  ax12el  39388  ax12inda  39394  ax12v2-o  39395  sn-exelALT  42660  relexp0eq  44128  ax6e2eq  44984  relopabVD  45327  ax6e2eqVD  45333  ormkglobd  47305  dtrucor3  49274