Theorem ax6ev 1991

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

Syntax hints:  ¬ wn 3  ∀wal 1560  ∃wex 1801

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

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

This theorem is referenced by:  equs4v  2022  alequexv  2023  equsv  2025  equid  2034  ax6evr  2037  aeveq  2080  sbcom2  2208  spimedv  2234  spimfv  2276  equsalv  2304  ax6e  2416  axc15  2455  sb4b  2508  dfeumo  2565  euequ  2626  dfdif3OLD  4074  exel  5403  dmi  5899  1st2val  8000  2nd2val  8001  elirrv  9547  bnj1468  35143  in-ax8  36589  ss-ax8  36590  bj-ssbeq  37130  bj-ax12  37134  bj-equsexval  37137  bj-ssbid2ALT  37140  bj-ax6elem2  37144  bj-spim0  37146  bj-eqs  37153  bj-equsvt  37251  bj-nnf-spime  37255  bj-spimtv  37284  bj-dtrucor2v  37307  bj-sbievw1  37335  bj-sbievw  37337  wl-isseteq  38004  wl-equsalvw  38046  wl-equsaldv  38048  wl-sbcom2d  38069  wl-euequf  38082  wl-dfclab  38093  axc11n-16  39567  ax12eq  39570  ax12el  39571  ax12inda  39577  ax12v2-o  39578  sn-exelALT  42843  relexp0eq  44282  ax6e2eq  45138  relopabVD  45481  ax6e2eqVD  45487  ormkglobd  47456  dtrucor3  49425