Theorem ax6ev 1969

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

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

This theorem is referenced by:  equs4v  1999  alequexv  2000  equsv  2002  equid  2011  ax6evr  2014  aeveq  2056  sbcom2  2173  spimedv  2197  spimfv  2239  equsalv  2267  ax6e  2388  axc15  2427  sb4b  2480  dfeumo  2537  euequ  2597  dfdif3OLD  4131  exel  5447  dmi  5939  1st2val  8050  2nd2val  8051  bnj1468  34853  in-ax8  36219  ss-ax8  36220  bj-ssbeq  36648  bj-ax12  36652  bj-equsexval  36655  bj-ssbid2ALT  36658  bj-ax6elem2  36662  bj-eqs  36670  bj-equsvt  36774  bj-spimtv  36789  bj-dtrucor2v  36812  bj-sbievw1  36840  bj-sbievw  36842  wl-isseteq  37500  wl-equsalvw  37533  wl-equsaldv  37535  wl-sbcom2d  37556  wl-euequf  37569  wl-dfclab  37591  axc11n-16  38934  ax12eq  38937  ax12el  38938  ax12inda  38944  ax12v2-o  38945  sn-exelALT  42250  relexp0eq  43707  ax6e2eq  44570  relopabVD  44914  ax6e2eqVD  44920  dtrucor3  48686