Theorem ax6ev 1970

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

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1780

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

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

This theorem is referenced by:  equs4v  2001  alequexv  2002  equsv  2004  equid  2013  ax6evr  2016  aeveq  2059  sbcom2  2176  spimedv  2200  spimfv  2242  equsalv  2270  ax6e  2383  axc15  2422  sb4b  2475  dfeumo  2532  euequ  2592  dfdif3OLD  4065  exel  5374  dmi  5860  1st2val  7949  2nd2val  7950  bnj1468  34858  in-ax8  36268  ss-ax8  36269  bj-ssbeq  36697  bj-ax12  36701  bj-equsexval  36704  bj-ssbid2ALT  36707  bj-ax6elem2  36711  bj-eqs  36719  bj-equsvt  36823  bj-spimtv  36838  bj-dtrucor2v  36861  bj-sbievw1  36889  bj-sbievw  36891  wl-isseteq  37549  wl-equsalvw  37582  wl-equsaldv  37584  wl-sbcom2d  37605  wl-euequf  37618  wl-dfclab  37629  axc11n-16  39036  ax12eq  39039  ax12el  39040  ax12inda  39046  ax12v2-o  39047  sn-exelALT  42310  relexp0eq  43793  ax6e2eq  44649  relopabVD  44992  ax6e2eqVD  44998  ormkglobd  46972  dtrucor3  48898