Theorem ax6ev 1977

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

Syntax hints:  ¬ wn 3  ∀wal 1546  ∃wex 1787

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

This theorem depends on definitions:  df-bi 209  df-ex 1788

This theorem is referenced by:  equs4v  2008  alequexv  2009  equsv  2011  equid  2020  ax6evr  2023  aeveq  2066  sbcom2  2185  spimedv  2211  spimfv  2253  equsalv  2281  ax6e  2393  axc15  2432  sb4b  2485  dfeumo  2542  euequ  2603  dfdif3OLD  4052  exel  5376  dmi  5870  1st2val  7963  2nd2val  7964  elirrv  9506  bnj1468  35043  in-ax8  36467  ss-ax8  36468  bj-ssbeq  37008  bj-ax12  37012  bj-equsexval  37015  bj-ssbid2ALT  37018  bj-ax6elem2  37022  bj-spim0  37024  bj-eqs  37031  bj-equsvt  37129  bj-nnf-spime  37133  bj-spimtv  37162  bj-dtrucor2v  37185  bj-sbievw1  37213  bj-sbievw  37215  wl-isseteq  37882  wl-equsalvw  37924  wl-equsaldv  37926  wl-sbcom2d  37947  wl-euequf  37960  wl-dfclab  37971  axc11n-16  39445  ax12eq  39448  ax12el  39449  ax12inda  39455  ax12v2-o  39456  sn-exelALT  42721  relexp0eq  44160  ax6e2eq  45016  relopabVD  45359  ax6e2eqVD  45365  ormkglobd  47334  dtrucor3  49303