Metamath Proof Explorer

Theorem ax6

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

This theorem should be referenced in place of ax-6 so that all proofs can be traced back to ax6v . Usage of this theorem is discouraged because it depends on ax-13 . When possible, use the weaker ax6v rather than ax6 since the ax6v 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) (New usage is discouraged.)

Ref Expression
Assertion ax6 ¬ x ¬ x = y


Step Hyp Ref Expression
1 ax6e x x = y
2 df-ex x x = y ¬ x ¬ x = y
3 1 2 mpbi ¬ x ¬ x = y