Theorem ax6ev 1999

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1809

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 1997

This proof depends on definitions:  df-bi 210  df-ex 1810

This theorem is used by:  equs4v  2030  alequexv  2031  equsv  2033  equid  2042  ax6evr  2045  aeveq  2088  sbcom2  2207  spimedv  2233  spimfv  2275  equsalv  2303  ax6e  2415  axc15  2454  sb4b  2507  dfeumo  2564  euequ  2625  dfdif3OLD  4073  exel  5415  dmi  5911  1st2val  8010  2nd2val  8011  elirrv  9555  bnj1468  35243  in-ax8  36764  ss-ax8  36765  bj-ssbeq  37303  bj-ax12  37307  bj-equsexval  37310  bj-ssbid2ALT  37313  bj-ax6elem2  37317  bj-spim0  37319  bj-eqs  37326  bj-equsvt  37424  bj-nnf-spime  37428  bj-spimtv  37457  bj-dtrucor2v  37480  bj-sbievw1  37508  bj-sbievw  37510  wl-isseteq  38179  wl-equsalvw  38221  wl-equsaldv  38223  wl-sbcom2d  38244  wl-euequf  38257  wl-dfclab  38268  axc11n-16  39740  ax12eq  39743  ax12el  39744  ax12inda  39750  ax12v2-o  39751  sn-exelALT  43018  relexp0eq  44455  ax6e2eq  45294  relopabVD  45637  ax6e2eqVD  45643  ormkglobd  47619  dtrucor3  49605