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 1784	. 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
3	1, 2	mpbir 230	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1783

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 1784

This theorem is referenced by:  equs4v  2004  alequexv  2005  equsv  2007  equid  2016  ax6evr  2019  aeveq  2060  sbcom2  2163  spimedv  2193  spimfv  2235  equsalv  2262  ax6e  2383  axc15  2422  sb4b  2475  sb4bOLD  2476  dfeumo  2537  euequ  2597  dfdif3  4045  dmi  5819  1st2val  7832  2nd2val  7833  bnj1468  32726  bj-ssbeq  34761  bj-ax12  34765  bj-equsexval  34768  bj-ssbid2ALT  34771  bj-ax6elem2  34775  bj-eqs  34783  bj-equsvt  34888  bj-spimtv  34903  bj-dtrucor2v  34927  bj-sbievw1  34956  bj-sbievw  34958  wl-equsalvw  35624  wl-sbcom2d  35643  wl-euequf  35656  wl-dfclab  35674  axc11n-16  36879  ax12eq  36882  ax12el  36883  ax12inda  36889  ax12v2-o  36890  sn-el  40115  relexp0eq  41198  ax6e2eq  42066  relopabVD  42410  ax6e2eqVD  42416  dtrucor3  46032