Theorem ax6ev 1969

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

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1777

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 1778

This theorem is referenced by:  equs4v  1999  alequexv  2000  equsv  2002  equid  2011  ax6evr  2014  aeveq  2056  sbcom2  2174  spimedv  2198  spimfv  2240  equsalv  2268  ax6e  2391  axc15  2430  sb4b  2483  dfeumo  2540  euequ  2600  dfdif3OLD  4141  exel  5453  dmi  5946  1st2val  8060  2nd2val  8061  bnj1468  34824  in-ax8  36192  ss-ax8  36193  bj-ssbeq  36621  bj-ax12  36625  bj-equsexval  36628  bj-ssbid2ALT  36631  bj-ax6elem2  36635  bj-eqs  36643  bj-equsvt  36747  bj-spimtv  36762  bj-dtrucor2v  36785  bj-sbievw1  36813  bj-sbievw  36815  wl-equsalvw  37494  wl-equsaldv  37496  wl-sbcom2d  37517  wl-euequf  37530  wl-dfclab  37552  axc11n-16  38896  ax12eq  38899  ax12el  38900  ax12inda  38906  ax12v2-o  38907  sn-exelALT  42213  relexp0eq  43665  ax6e2eq  44530  relopabVD  44874  ax6e2eqVD  44880  dtrucor3  48534