Theorem ax6ev 1970

Description: At least one individual exists. Weaker version of ax6e 2385. When possible, use of this theorem rather than ax6e 2385 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  2178  spimedv  2202  spimfv  2244  equsalv  2272  ax6e  2385  axc15  2424  sb4b  2477  dfeumo  2534  euequ  2595  dfdif3OLD  4068  exel  5381  dmi  5868  1st2val  7959  2nd2val  7960  bnj1468  34951  in-ax8  36367  ss-ax8  36368  bj-ssbeq  36797  bj-ax12  36801  bj-equsexval  36804  bj-ssbid2ALT  36807  bj-ax6elem2  36811  bj-eqs  36819  bj-equsvt  36923  bj-spimtv  36938  bj-dtrucor2v  36961  bj-sbievw1  36989  bj-sbievw  36991  wl-isseteq  37649  wl-equsalvw  37682  wl-equsaldv  37684  wl-sbcom2d  37705  wl-euequf  37718  wl-dfclab  37729  axc11n-16  39137  ax12eq  39140  ax12el  39141  ax12inda  39147  ax12v2-o  39148  sn-exelALT  42416  relexp0eq  43884  ax6e2eq  44740  relopabVD  45083  ax6e2eqVD  45089  ormkglobd  47061  dtrucor3  48986