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  4115  exel  5434  dmi  5922  1st2val  8003  2nd2val  8004  bnj1468  33857  bj-ssbeq  35530  bj-ax12  35534  bj-equsexval  35537  bj-ssbid2ALT  35540  bj-ax6elem2  35544  bj-eqs  35552  bj-equsvt  35657  bj-spimtv  35672  bj-dtrucor2v  35695  bj-sbievw1  35724  bj-sbievw  35726  wl-equsalvw  36407  wl-sbcom2d  36426  wl-euequf  36439  wl-dfclab  36458  axc11n-16  37808  ax12eq  37811  ax12el  37812  ax12inda  37818  ax12v2-o  37819  sn-exelALT  41035  relexp0eq  42452  ax6e2eq  43318  relopabVD  43662  ax6e2eqVD  43668  dtrucor3  47484