Theorem ax6ev 2004

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 2003	. 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2		df-ex 1813	. 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
3	1, 2	mpbir 234	1 ⊢ ∃𝑥 𝑥 = 𝑦

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

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

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

This theorem is used by:  equs4v  2035  alequexv  2036  equsv  2038  equid  2047  ax6evr  2050  aeveq  2093  sbcom2  2212  spimedv  2237  spimfv  2279  equsalv  2305  ax6e  2415  axc15  2454  sb4b  2507  dfeumo  2564  euequ  2625  exel  5406  dmi  5909  1st2val  8050  2nd2val  8051  elirrv  9615  bnj1468  35543  in-ax8  37190  ss-ax8  37191  bj-ssbeq  37729  bj-ax12  37733  bj-equsexval  37736  bj-ssbid2ALT  37739  bj-ax6elem2  37743  bj-spim0  37745  bj-eqs  37752  bj-equsvt  37850  bj-nnf-spime  37854  bj-spimtv  37883  bj-dtrucor2v  37906  bj-sbievw1  37934  bj-sbievw  37936  wl-isseteq  38619  wl-equsalvw  38661  wl-equsaldv  38663  wl-sbcom2d  38684  wl-euequf  38697  wl-dfclab  38708  axc11n-16  40186  ax12eq  40189  ax12el  40190  ax12inda  40196  ax12v2-o  40197  sn-exelALT  43464  relexp0eq  44891  ax6e2eq  45729  relopabVD  46072  ax6e2eqVD  46078  ormkglobd  48090  dtrucor3  50112