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  4071  exel  5384  dmi  5871  1st2val  7963  2nd2val  7964  bnj1468  35004  in-ax8  36420  ss-ax8  36421  bj-ssbeq  36856  bj-ax12  36860  bj-equsexval  36863  bj-ssbid2ALT  36866  bj-ax6elem2  36870  bj-eqs  36878  bj-equsvt  36982  bj-spimtv  36997  bj-dtrucor2v  37020  bj-sbievw1  37048  bj-sbievw  37050  wl-isseteq  37712  wl-equsalvw  37745  wl-equsaldv  37747  wl-sbcom2d  37768  wl-euequf  37781  wl-dfclab  37792  axc11n-16  39266  ax12eq  39269  ax12el  39270  ax12inda  39276  ax12v2-o  39277  sn-exelALT  42543  relexp0eq  44009  ax6e2eq  44865  relopabVD  45208  ax6e2eqVD  45214  ormkglobd  47186  dtrucor3  49111