Theorem ax6ev 1974

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

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1782

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

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

This theorem is referenced by:  equs4v  2004  alequexv  2005  equsv  2007  equid  2016  ax6evr  2019  aeveq  2060  sbcom2  2162  spimedv  2191  spimfv  2233  equsalv  2259  ax6e  2383  axc15  2422  sb4b  2475  dfeumo  2532  euequ  2592  dfdif3  4114  exel  5433  dmi  5920  1st2val  8000  2nd2val  8001  bnj1468  33846  bj-ssbeq  35519  bj-ax12  35523  bj-equsexval  35526  bj-ssbid2ALT  35529  bj-ax6elem2  35533  bj-eqs  35541  bj-equsvt  35646  bj-spimtv  35661  bj-dtrucor2v  35684  bj-sbievw1  35713  bj-sbievw  35715  wl-equsalvw  36396  wl-sbcom2d  36415  wl-euequf  36428  wl-dfclab  36447  axc11n-16  37797  ax12eq  37800  ax12el  37801  ax12inda  37807  ax12v2-o  37808  sn-exelALT  41032  relexp0eq  42438  ax6e2eq  43304  relopabVD  43648  ax6e2eqVD  43654  dtrucor3  47438