Theorem ax6ev 1968

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

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1778

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

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  equs4v  1998  alequexv  1999  equsv  2001  equid  2010  ax6evr  2013  aeveq  2055  sbcom2  2172  spimedv  2196  spimfv  2238  equsalv  2266  ax6e  2386  axc15  2425  sb4b  2478  dfeumo  2535  euequ  2595  dfdif3OLD  4098  exel  5418  dmi  5912  1st2val  8024  2nd2val  8025  bnj1468  34819  in-ax8  36184  ss-ax8  36185  bj-ssbeq  36613  bj-ax12  36617  bj-equsexval  36620  bj-ssbid2ALT  36623  bj-ax6elem2  36627  bj-eqs  36635  bj-equsvt  36739  bj-spimtv  36754  bj-dtrucor2v  36777  bj-sbievw1  36805  bj-sbievw  36807  wl-isseteq  37465  wl-equsalvw  37498  wl-equsaldv  37500  wl-sbcom2d  37521  wl-euequf  37534  wl-dfclab  37556  axc11n-16  38898  ax12eq  38901  ax12el  38902  ax12inda  38908  ax12v2-o  38909  sn-exelALT  42216  relexp0eq  43676  ax6e2eq  44534  relopabVD  44878  ax6e2eqVD  44884  ormkglobd  46847  dtrucor3  48677