MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax6ev Unicode version

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
StepHypRef Expression
1 ax6v 1748 . 2
2 df-ex 1613 . 2
31, 2mpbir 209 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator