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

Theorem ax6ev 2048
Description: At least one individual exists. Weaker version of ax6e 2387. When possible, use of this theorem rather than ax6e 2387 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 2047 . 2 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2 df-ex 1846 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbir 221 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1622  wex 1845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-6 2046
This theorem depends on definitions:  df-bi 197  df-ex 1846
This theorem is referenced by:  exiftru  2049  spimeh  2072  equs4v  2077  equsalvw  2078  equsexvw  2079  equid  2086  ax6evr  2089  equvinv  2104  aeveq  2125  19.8a  2191  equsalv  2247  equsexv  2248  spimv1  2254  equsalhw  2262  ax6e  2387  axc15  2440  axc11nOLD  2444  sbcom2  2574  euex  2623  axext3  2734  dfdif3  3855  dmi  5487  snnexOLD  7124  1st2val  7353  2nd2val  7354  bnj1468  31215  bj-sbex  32924  bj-ssbeq  32925  bj-ssb0  32926  bj-ssb1  32931  bj-equsexval  32936  bj-ssbid2ALT  32944  bj-ax6elem2  32950  bj-alequexv  32953  bj-eqs  32961  bj-spimtv  33016  bj-spimedv  33017  bj-spimvv  33019  bj-speiv  33022  bj-dtrucor2v  33099  bj-cleljustab  33145  wl-sbcom2d  33649  wl-euequ1f  33661  axc11n-16  34719  ax12eq  34722  ax12el  34723  ax12inda  34729  ax12v2-o  34730  relexp0eq  38487  ax6e2eq  39267  relopabVD  39628  ax6e2eqVD  39634
  Copyright terms: Public domain W3C validator