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  5905  1st2val  8015  2nd2val  8016  elirrv  9572  bnj1468  35358  in-ax8  36847  ss-ax8  36848  bj-ssbeq  37386  bj-ax12  37390  bj-equsexval  37393  bj-ssbid2ALT  37396  bj-ax6elem2  37400  bj-spim0  37402  bj-eqs  37409  bj-equsvt  37507  bj-nnf-spime  37511  bj-spimtv  37540  bj-dtrucor2v  37563  bj-sbievw1  37591  bj-sbievw  37593  wl-isseteq  38262  wl-equsalvw  38304  wl-equsaldv  38306  wl-sbcom2d  38327  wl-euequf  38340  wl-dfclab  38351  axc11n-16  39814  ax12eq  39817  ax12el  39818  ax12inda  39824  ax12v2-o  39825  sn-exelALT  43092  relexp0eq  44544  ax6e2eq  45383  relopabVD  45726  ax6e2eqVD  45732  ormkglobd  47708  dtrucor3  49730