Theorem ax6ev 1972

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

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1780

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

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  spimehOLD  1975  exgenOLD  1979  equs4v  2006  alequexv  2007  equsv  2009  equsexvwOLD  2012  equid  2019  ax6evr  2022  aeveq  2061  spsbeOLD  2089  sbcom2  2168  spimedv  2197  spimfv  2241  equsalv  2268  equsexv  2269  ax6e  2401  axc15  2444  sb4b  2499  sb4bOLD  2500  equsb1vOLDOLD  2517  sbtvOLD  2519  dfeumo  2619  euequ  2683  dfdif3  4093  dmi  5793  1st2val  7719  2nd2val  7720  bnj1468  32120  bj-ssbeq  33988  bj-ax12  33992  bj-equsexval  33995  bj-ssbid2ALT  33998  bj-ax6elem2  34002  bj-eqs  34010  bj-spimtv  34118  bj-dtrucor2v  34142  bj-sbievw1  34171  bj-sbievw  34173  wl-equsalvw  34780  wl-sbcom2d  34799  wl-euequf  34812  wl-dfclab  34830  axc11n-16  36076  ax12eq  36079  ax12el  36080  ax12inda  36086  ax12v2-o  36087  sn-el  39117  relexp0eq  40053  ax6e2eq  40898  relopabVD  41242  ax6e2eqVD  41248