# 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 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$

### Proof

Step Hyp Ref Expression
1 ax6e ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
2 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
3 1 2 mpbi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$