Theorem ax6ev 2002

Description: At least one individual exists. Weaker version of ax6e 2412. When possible, use of this theorem rather than ax6e 2412 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 2001	. 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 2000

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

This theorem is used by:  equs4v  2033  alequexv  2034  equsv  2036  equid  2045  ax6evr  2048  aeveq  2091  sbcom2  2209  spimedv  2233  spimfv  2275  equsalv  2301  ax6e  2412  axc15  2451  sb4b  2504  dfeumo  2561  euequ  2622  exel  5409  dmi  5907  1st2val  8020  2nd2val  8021  elirrv  9576  bnj1468  35388  in-ax8  36911  ss-ax8  36912  bj-ssbeq  37450  bj-ax12  37454  bj-equsexval  37457  bj-ssbid2ALT  37460  bj-ax6elem2  37464  bj-spim0  37466  bj-eqs  37473  bj-equsvt  37571  bj-nnf-spime  37575  bj-spimtv  37604  bj-dtrucor2v  37627  bj-sbievw1  37655  bj-sbievw  37657  wl-isseteq  38324  wl-equsalvw  38366  wl-equsaldv  38368  wl-sbcom2d  38389  wl-euequf  38402  wl-dfclab  38413  axc11n-16  39876  ax12eq  39879  ax12el  39880  ax12inda  39886  ax12v2-o  39887  sn-exelALT  43154  relexp0eq  44606  ax6e2eq  45445  relopabVD  45788  ax6e2eqVD  45794  ormkglobd  47770  dtrucor3  49792