Theorem ax6ev 1890

Description: At least one individual exists. Weaker version of ax6e 2250. When possible, use of this theorem rather than ax6e 2250 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)

Assertion

Ref	Expression
ax6ev	|- E. x x = y

Distinct variable group:   x, y

Proof of Theorem ax6ev

Step	Hyp	Ref	Expression
1		ax6v 1889	. 2 |- -. A. x -. x = y
2		df-ex 1705	. 2 |- ( E. x x = y <-> -. A. x -. x = y )
3	1, 2	mpbir 221	1 |- E. x x = y

Syntax hints:   -. wn 3   A.wal 1481   E.wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  exiftru  1891  spimeh  1925  equs4v  1930  equsalvw  1931  equsexvw  1932  equid  1939  ax6evr  1942  equvinv  1959  equvinivOLD  1961  aeveq  1982  ax12vOLDOLD  2051  19.8a  2052  equsalv  2108  equsexv  2109  spimv1  2115  equsalhw  2123  aevOLD  2162  ax6e  2250  axc15  2303  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  ax12v2OLD  2342  sbcom2  2445  euex  2494  axext3  2604  dmi  5340  snnexOLD  6967  1st2val  7194  2nd2val  7195  bnj1468  30916  bj-sbex  32626  bj-ssbeq  32627  bj-ssb0  32628  bj-ssb1  32633  bj-equsexval  32638  bj-ssbid2ALT  32646  bj-ax6elem2  32652  bj-alequexv  32655  bj-eqs  32663  bj-spimtv  32718  bj-spimedv  32719  bj-spimvv  32721  bj-speiv  32724  bj-dtrucor2v  32801  bj-cleljustab  32847  wl-sbcom2d  33344  wl-euequ1f  33356  axc11n-16  34223  ax12eq  34226  ax12el  34227  ax12inda  34233  ax12v2-o  34234  relexp0eq  37993  ax6e2eq  38773  relopabVD  39137  ax6e2eqVD  39143