Theorem ax6ev 2048

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

Syntax hints:  ¬ wn 3  ∀wal 1622  ∃wex 1845

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

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

This theorem is referenced by:  exiftru  2049  spimeh  2072  equs4v  2077  equsalvw  2078  equsexvw  2079  equid  2086  ax6evr  2089  equvinv  2104  aeveq  2125  19.8a  2191  equsalv  2247  equsexv  2248  spimv1  2254  equsalhw  2262  ax6e  2387  axc15  2440  axc11nOLD  2444  sbcom2  2574  euex  2623  axext3  2734  dfdif3  3855  dmi  5487  snnexOLD  7124  1st2val  7353  2nd2val  7354  bnj1468  31215  bj-sbex  32924  bj-ssbeq  32925  bj-ssb0  32926  bj-ssb1  32931  bj-equsexval  32936  bj-ssbid2ALT  32944  bj-ax6elem2  32950  bj-alequexv  32953  bj-eqs  32961  bj-spimtv  33016  bj-spimedv  33017  bj-spimvv  33019  bj-speiv  33022  bj-dtrucor2v  33099  bj-cleljustab  33145  wl-sbcom2d  33649  wl-euequ1f  33661  axc11n-16  34719  ax12eq  34722  ax12el  34723  ax12inda  34729  ax12v2-o  34730  relexp0eq  38487  ax6e2eq  39267  relopabVD  39628  ax6e2eqVD  39634