Theorem ax6ev 1892

Description: At least one individual exists. Weaker version of ax6e 2254. When possible, use of this theorem rather than ax6e 2254 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 1891	. 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 1890

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

This theorem is referenced by:  exiftru  1893  spimeh  1927  equs4v  1932  equsalvw  1933  equsexvw  1934  equid  1941  ax6evr  1944  equvinv  1961  equvinivOLD  1963  aeveq  1984  ax12vOLDOLD  2053  19.8a  2054  19.8aOLD  2055  equsexv  2111  spimv1  2117  equsalhw  2125  aevOLD  2164  cbv3hvOLD  2177  cbv3hvOLDOLD  2178  ax6e  2254  axc15  2307  axc11nOLD  2312  axc11nOLDOLD  2313  axc11nALT  2314  ax12v2OLD  2346  sbcom2  2449  euex  2498  axext3  2608  dmi  5304  snnex  6918  1st2val  7142  2nd2val  7143  bnj1468  30616  bj-sbex  32260  bj-ssbeq  32261  bj-ssb0  32262  bj-ssb1  32267  bj-equsexval  32272  bj-ssbid2ALT  32280  bj-ax6elem2  32286  bj-alequexv  32289  bj-eqs  32297  bj-spimtv  32352  bj-spimedv  32353  bj-spimvv  32355  bj-speiv  32358  bj-equsalv  32378  bj-dtrucor2v  32436  bj-cleljustab  32484  wl-sbcom2d  32971  wl-euequ1f  32983  axc11n-16  33689  ax12eq  33692  ax12el  33693  ax12inda  33699  ax12v2-o  33700  relexp0eq  37460  ax6e2eq  38241  relopabVD  38606  ax6e2eqVD  38612