Theorem ax6ev 1966

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

Syntax hints:  ¬ wn 3  ∀wal 1532  ∃wex 1774

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

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  equs4v  1996  alequexv  1997  equsv  1999  equid  2008  ax6evr  2011  aeveq  2052  sbcom2  2154  spimedv  2183  spimfv  2225  equsalv  2251  ax6e  2377  axc15  2416  sb4b  2469  dfeumo  2526  euequ  2586  dfdif3  4110  exel  5429  dmi  5918  1st2val  8015  2nd2val  8016  bnj1468  34413  bj-ssbeq  36065  bj-ax12  36069  bj-equsexval  36072  bj-ssbid2ALT  36075  bj-ax6elem2  36079  bj-eqs  36087  bj-equsvt  36192  bj-spimtv  36207  bj-dtrucor2v  36230  bj-sbievw1  36258  bj-sbievw  36260  wl-equsalvw  36941  wl-sbcom2d  36963  wl-euequf  36976  wl-dfclab  36998  axc11n-16  38347  ax12eq  38350  ax12el  38351  ax12inda  38357  ax12v2-o  38358  sn-exelALT  41626  relexp0eq  43054  ax6e2eq  43919  relopabVD  44263  ax6e2eqVD  44269  dtrucor3  47794