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  4072  exel  5392  dmi  5880  1st2val  7973  2nd2val  7974  bnj1468  35028  in-ax8  36446  ss-ax8  36447  bj-ssbeq  36915  bj-ax12  36919  bj-equsexval  36922  bj-ssbid2ALT  36925  bj-ax6elem2  36929  bj-spim0  36931  bj-eqs  36938  bj-equsvt  37036  bj-nnf-spime  37040  bj-spimtv  37069  bj-dtrucor2v  37092  bj-sbievw1  37120  bj-sbievw  37122  wl-isseteq  37787  wl-equsalvw  37822  wl-equsaldv  37824  wl-sbcom2d  37845  wl-euequf  37858  wl-dfclab  37869  axc11n-16  39343  ax12eq  39346  ax12el  39347  ax12inda  39353  ax12v2-o  39354  sn-exelALT  42620  relexp0eq  44086  ax6e2eq  44942  relopabVD  45285  ax6e2eqVD  45291  ormkglobd  47262  dtrucor3  49187