Theorem ax6ev 1971

Description: At least one individual exists. Weaker version of ax6e 2388. When possible, use of this theorem rather than ax6e 2388 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  2388  axc15  2427  sb4b  2480  dfeumo  2537  euequ  2598  dfdif3OLD  4059  exel  5383  dmi  5872  1st2val  7965  2nd2val  7966  bnj1468  35008  in-ax8  36426  ss-ax8  36427  bj-ssbeq  36967  bj-ax12  36971  bj-equsexval  36974  bj-ssbid2ALT  36977  bj-ax6elem2  36981  bj-spim0  36983  bj-eqs  36990  bj-equsvt  37088  bj-nnf-spime  37092  bj-spimtv  37121  bj-dtrucor2v  37144  bj-sbievw1  37172  bj-sbievw  37174  wl-isseteq  37839  wl-equsalvw  37881  wl-equsaldv  37883  wl-sbcom2d  37904  wl-euequf  37917  wl-dfclab  37928  axc11n-16  39402  ax12eq  39405  ax12el  39406  ax12inda  39412  ax12v2-o  39413  sn-exelALT  42678  relexp0eq  44150  ax6e2eq  45006  relopabVD  45349  ax6e2eqVD  45355  ormkglobd  47325  dtrucor3  49290