Theorem ax6ev 1887

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

Syntax hints:  ¬ wn 3  ∀wal 1478  ∃wex 1701

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

This theorem depends on definitions:  df-bi 197  df-ex 1702

This theorem is referenced by:  exiftru  1888  spimeh  1922  equs4v  1927  equsalvw  1928  equsexvw  1929  equid  1936  ax6evr  1939  equvinv  1956  equvinivOLD  1958  aeveq  1979  ax12vOLDOLD  2048  19.8a  2049  19.8aOLD  2050  equsexv  2106  spimv1  2112  equsalhw  2120  aevOLD  2159  cbv3hvOLD  2172  cbv3hvOLDOLD  2173  ax6e  2249  axc15  2302  axc11nOLD  2307  axc11nOLDOLD  2308  axc11nALT  2309  ax12v2OLD  2341  sbcom2  2444  euex  2493  axext3  2603  dmi  5310  snnexOLD  6931  1st2val  7154  2nd2val  7155  bnj1468  30677  bj-sbex  32321  bj-ssbeq  32322  bj-ssb0  32323  bj-ssb1  32328  bj-equsexval  32333  bj-ssbid2ALT  32341  bj-ax6elem2  32347  bj-alequexv  32350  bj-eqs  32358  bj-spimtv  32413  bj-spimedv  32414  bj-spimvv  32416  bj-speiv  32419  bj-equsalv  32439  bj-dtrucor2v  32497  bj-cleljustab  32545  wl-sbcom2d  33015  wl-euequ1f  33027  axc11n-16  33742  ax12eq  33745  ax12el  33746  ax12inda  33752  ax12v2-o  33753  relexp0eq  37513  ax6e2eq  38294  relopabVD  38659  ax6e2eqVD  38665