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

Theorem ax6 2142
Description: Theorem showing that ax-6 1838 follows from the weaker version ax6v 1839. (Even though this theorem depends on ax-6 1838, all references of ax-6 1838 are made via ax6v 1839. An earlier version stated ax6v 1839 as a separate axiom, but having two axioms caused some confusion.)

This theorem should be referenced in place of ax-6 1838 so that all proofs can be traced back to ax6v 1839. When possible, use the weaker ax6v 1839 rather than ax6 2142 since the ax6v 1839 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.)

Assertion
Ref Expression
ax6 ¬ ∀𝑥 ¬ 𝑥 = 𝑦

Proof of Theorem ax6
StepHypRef Expression
1 ax6e 2141 . 2 𝑥 𝑥 = 𝑦
2 df-ex 1695 . 2 (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦)
31, 2mpbi 218 1 ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983  ax-13 2137
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  axc10  2143
  Copyright terms: Public domain W3C validator