Theorem ax6ev 1749

Description: At least one individual exists. Weaker version of ax6e 2002. When possible, use of this theorem rather than ax6e 2002 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 1748	. 2
2		df-ex 1613	. 2
3	1, 2	mpbir 209	1

Syntax hints:  -.wn 3  A.wal 1393  E.wex 1612

This theorem is referenced by:  exiftru  1750  spimeh  1782  equs4v  1787  equid  1791  equviniv  1803  ax12v  1855  ax12vOLD  1856  19.8a  1857  19.8aOLD  1858  aev  1943  equsalhw  1945  cbv3hv  1956  ax6e  2002  axc11n  2049  axc11nOLD  2050  ax12v2  2083  sbcom2  2189  axc11n-16  2268  ax12eq  2271  ax12el  2272  ax12inda  2278  ax12v2-o  2279  euequ1  2288  euex  2308  euequ1OLD  2387  axext3  2437  relop  5158  dmi  5222  snnex  6606  1st2val  6826  2nd2val  6827  wl-sbcom2d  30011  ax6e2eq  33330  relopabVD  33701  ax6e2eqVD  33707  bnj1468  33904  bj-spimtv  34278  bj-spimv  34279  bj-spimedv  34280  bj-speiv  34285  bj-equsalv  34309  bj-equsalvv  34310  bj-axc11nv  34316  bj-axc15v  34330  bj-dtrucor2v  34387

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

This theorem depends on definitions:  df-bi 185  df-ex 1613