Theorem ax6ev 1965

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

Syntax hints:  ¬ wn 3  ∀wal 1531  ∃wex 1773

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

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

This theorem is referenced by:  equs4v  1995  alequexv  1996  equsv  1998  equid  2007  ax6evr  2010  aeveq  2051  sbcom2  2162  spimedv  2185  spimfv  2227  equsalv  2253  ax6e  2376  axc15  2415  sb4b  2468  dfeumo  2525  euequ  2585  dfdif3  4111  exel  5434  dmi  5923  1st2val  8020  2nd2val  8021  bnj1468  34547  bj-ssbeq  36199  bj-ax12  36203  bj-equsexval  36206  bj-ssbid2ALT  36209  bj-ax6elem2  36213  bj-eqs  36221  bj-equsvt  36326  bj-spimtv  36341  bj-dtrucor2v  36364  bj-sbievw1  36392  bj-sbievw  36394  wl-equsalvw  37075  wl-equsaldv  37077  wl-sbcom2d  37098  wl-euequf  37111  wl-dfclab  37133  axc11n-16  38479  ax12eq  38482  ax12el  38483  ax12inda  38489  ax12v2-o  38490  sn-exelALT  41775  relexp0eq  43196  ax6e2eq  44061  relopabVD  44405  ax6e2eqVD  44411  dtrucor3  47983